Metamath Proof Explorer


Theorem unieqOLD

Description: Obsolete version of unieq as of 13-Apr-2024. (Contributed by NM, 10-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.) 29-Jun-2011.)

Ref Expression
Assertion unieqOLD A = B A = B

Proof

Step Hyp Ref Expression
1 rexeq A = B x A y x x B y x
2 1 abbidv A = B y | x A y x = y | x B y x
3 dfuni2 A = y | x A y x
4 dfuni2 B = y | x B y x
5 2 3 4 3eqtr4g A = B A = B