This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \emptyset \leftrightarrow A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ A \approx \emptyset \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} \emptyset$
2		f1ocnv	$⊢ f : A \underset{1-1 onto}{⟶} \emptyset \to f^{-1} : \emptyset \underset{1-1 onto}{⟶} A$
3		f1o00	$⊢ f^{-1} : \emptyset \underset{1-1 onto}{⟶} A \leftrightarrow (f^{-1} = \emptyset \land A = \emptyset)$
4	3	simprbi	$⊢ f^{-1} : \emptyset \underset{1-1 onto}{⟶} A \to A = \emptyset$
5	2 4	syl	$⊢ f : A \underset{1-1 onto}{⟶} \emptyset \to A = \emptyset$
6	5	exlimiv	$⊢ \exists f f : A \underset{1-1 onto}{⟶} \emptyset \to A = \emptyset$
7	1 6	sylbi	$⊢ A \approx \emptyset \to A = \emptyset$
8		0ex	$⊢ \emptyset \in V$
9	8	enref	$⊢ \emptyset \approx \emptyset$
10		breq1	$⊢ A = \emptyset \to (A \approx \emptyset \leftrightarrow \emptyset \approx \emptyset)$
11	9 10	mpbiri	$⊢ A = \emptyset \to A \approx \emptyset$
12	7 11	impbii	$⊢ A \approx \emptyset \leftrightarrow A = \emptyset$