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	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 } ≈ { 𝐵 } )