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 ( 𝐴 = 𝐵 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 rexeq ( 𝐴 = 𝐵 → ( ∃ 𝑥𝐴 𝑦𝑥 ↔ ∃ 𝑥𝐵 𝑦𝑥 ) )
2 1 abbidv ( 𝐴 = 𝐵 → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦𝑥 } = { 𝑦 ∣ ∃ 𝑥𝐵 𝑦𝑥 } )
3 dfuni2 𝐴 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦𝑥 }
4 dfuni2 𝐵 = { 𝑦 ∣ ∃ 𝑥𝐵 𝑦𝑥 }
5 2 3 4 3eqtr4g ( 𝐴 = 𝐵 𝐴 = 𝐵 )