Metamath Proof Explorer


Theorem en2snOLDOLD

Description: Obsolete version of en2sn as of 31-Jul-2024. (Contributed by NM, 9-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ensn1g ( 𝐴𝐶 → { 𝐴 } ≈ 1o )
2 ensn1g ( 𝐵𝐷 → { 𝐵 } ≈ 1o )
3 2 ensymd ( 𝐵𝐷 → 1o ≈ { 𝐵 } )
4 entr ( ( { 𝐴 } ≈ 1o ∧ 1o ≈ { 𝐵 } ) → { 𝐴 } ≈ { 𝐵 } )
5 1 3 4 syl2an ( ( 𝐴𝐶𝐵𝐷 ) → { 𝐴 } ≈ { 𝐵 } )