Theorem en0OLD

Description: Obsolete version of en0 as of 23-Sep-2024. (Contributed by NM, 27-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	en0OLD	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		bren	$$⊢A\approx \varnothing \leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}\varnothing$$
2		f1ocnv	$$⊢f:A\underset{1-1\; onto}{⟶}\varnothing \to f^{-1}:\varnothing \underset{1-1\; onto}{⟶}A$$
3		f1o00	$$⊢f^{-1}:\varnothing \underset{1-1\; onto}{⟶}A\leftrightarrow \left(f^{-1}=\varnothing \wedge A=\varnothing \right)$$
4	3	simprbi	$$⊢f^{-1}:\varnothing \underset{1-1\; onto}{⟶}A\to A=\varnothing$$
5	2 4	syl	$$⊢f:A\underset{1-1\; onto}{⟶}\varnothing \to A=\varnothing$$
6	5	exlimiv	$$⊢\exists ff:A\underset{1-1\; onto}{⟶}\varnothing \to A=\varnothing$$
7	1 6	sylbi	$$⊢A\approx \varnothing \to A=\varnothing$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9		f1oeq1	$$⊢f=\varnothing \to \left(f:\varnothing \underset{1-1\; onto}{⟶}\varnothing \leftrightarrow \varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing \right)$$
10		f1o0	$$⊢\varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing$$
11	8 9 10	ceqsexv2d	$$⊢\exists ff:\varnothing \underset{1-1\; onto}{⟶}\varnothing$$
12		bren	$$⊢\varnothing \approx \varnothing \leftrightarrow \exists ff:\varnothing \underset{1-1\; onto}{⟶}\varnothing$$
13	11 12	mpbir	$$⊢\varnothing \approx \varnothing$$
14		breq1	$$⊢A=\varnothing \to \left(A\approx \varnothing \leftrightarrow \varnothing \approx \varnothing \right)$$
15	13 14	mpbiri	$$⊢A=\varnothing \to A\approx \varnothing$$
16	7 15	impbii	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$