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
|- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } )

Proof

Step Hyp Ref Expression
1 ensn1g
 |-  ( A e. C -> { A } ~~ 1o )
2 ensn1g
 |-  ( B e. D -> { B } ~~ 1o )
3 2 ensymd
 |-  ( B e. D -> 1o ~~ { B } )
4 entr
 |-  ( ( { A } ~~ 1o /\ 1o ~~ { B } ) -> { A } ~~ { B } )
5 1 3 4 syl2an
 |-  ( ( A e. C /\ B e. D ) -> { A } ~~ { B } )