Theorem en2snOLD

Description: Obsolete version of en2sn as of 25-Sep-2024. (Contributed by NM, 9-Nov-2003) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	en2snOLD	$$⊢\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		bren	$$⊢\left\{A\right\}\approx \left\{B\right\}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
7	5 6	sylibr	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A\right\}\approx \left\{B\right\}$$