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 } ) |
| 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 } ) |