Metamath Proof Explorer


Theorem en2snOLD

Description: Obsolete version of en2sn as of 25-Sep-2024. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en2snOLD ( ( 𝐴𝐶𝐵𝐷 ) → { 𝐴 } ≈ { 𝐵 } )

Proof

Step Hyp Ref Expression
1 snex { ⟨ 𝐴 , 𝐵 ⟩ } ∈ V
2 f1osng ( ( 𝐴𝐶𝐵𝐷 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } )
3 f1oeq1 ( 𝑓 = { ⟨ 𝐴 , 𝐵 ⟩ } → ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
4 3 spcegv ( { ⟨ 𝐴 , 𝐵 ⟩ } ∈ V → ( { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } → ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
5 1 2 4 mpsyl ( ( 𝐴𝐶𝐵𝐷 ) → ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } )
6 bren ( { 𝐴 } ≈ { 𝐵 } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { 𝐵 } )
7 5 6 sylibr ( ( 𝐴𝐶𝐵𝐷 ) → { 𝐴 } ≈ { 𝐵 } )