Theorem en2sn

Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003)

	Ref	Expression
Assertion	en2sn	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 } ≈ { 𝐵 } )

Proof

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