Theorem en2sn

Description: Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) Avoid ax-un . (Revised by BTernaryTau, 25-Sep-2024)

	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		snex	$$⊢\left\{⟨A,B⟩\right\}\in \mathrm{V}$$
2		f1osng	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
3		f1oeq1	$$⊢f=\left\{⟨A,B⟩\right\}\to \left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\leftrightarrow \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
4	3	spcegv	$$⊢\left\{⟨A,B⟩\right\}\in \mathrm{V}\to \left(\left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\to \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
5	1 2 4	mpsyl	$$⊢\left(A\in C\wedge B\in D\right)\to \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
6		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
7		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
8		breng	$$⊢\left(\left\{A\right\}\in \mathrm{V}\wedge \left\{B\right\}\in \mathrm{V}\right)\to \left(\left\{A\right\}\approx \left\{B\right\}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
9	6 7 8	mp2an	$$⊢\left\{A\right\}\approx \left\{B\right\}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
10	5 9	sylibr	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A\right\}\approx \left\{B\right\}$$