Theorem en2sn

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

	Ref	Expression
Assertion	en2sn	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A\right\}\approx \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ensn1g	$$⊢A\in C\to \left\{A\right\}\approx 1_{𝑜}$$
2		ensn1g	$$⊢B\in D\to \left\{B\right\}\approx 1_{𝑜}$$
3	2	ensymd	$$⊢B\in D\to 1_{𝑜}\approx \left\{B\right\}$$
4		entr	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge 1_{𝑜}\approx \left\{B\right\}\right)\to \left\{A\right\}\approx \left\{B\right\}$$
5	1 3 4	syl2an	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A\right\}\approx \left\{B\right\}$$