The argument you present is correct given the first two statements as premises. From those two statements one can derive using equality elimination and introduction both the third and fourth statement.
To see this, symbolize the names as follows:
- Let a be "Russia".
- Let b be "Russian Federation".
- Let c be "Russian Empire".
The following uses Klement's proof checker and natural deduction using rules for identity found in forallx, section 27.4:
Lines 1 and 2 symbolize the first two lines viewed as premises:
- Russia = Russian Federation [says so in the Constitution]
- Russian Federation ≠ Russian Empire
Line 3 results from taking the assumed identity in line 1 and substituting in line 2 b for a. This is the symbolization of the third statement:
- Russia ≠ Russian Empire [by substitution]
Line 8 after going through a subproof shows that the fourth statement using the symbolization above can be derived.
- Russian Empire ≠ Russia [by reflexivity of equality]
The subproof may require some explanation. On line 5 the identity a = a is introduced. Such a line may be introduced anywhere without reference to prior lines. Using the assumed identity on line 4, I can substitute the second a in line 5 with c to get line 6. This contradicts line 3 which allows me to introduce a contradiction on line 8 which is the desired result.
References
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/