Theorem en0ALT

Description: Shorter proof of en0 , depending on ax-pow and ax-un . (Contributed by NM, 27-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	en0ALT	$$⊢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	8	enref	$$⊢\varnothing \approx \varnothing$$
10		breq1	$$⊢A=\varnothing \to \left(A\approx \varnothing \leftrightarrow \varnothing \approx \varnothing \right)$$
11	9 10	mpbiri	$$⊢A=\varnothing \to A\approx \varnothing$$
12	7 11	impbii	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$