Metamath Proof Explorer

Theorem en0r

Description: The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024)

		Ref	Expression
	Assertion	en0r	$⊢ \emptyset \approx A \leftrightarrow A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		encv	$⊢ \emptyset \approx A \to (\emptyset \in V \land A \in V)$
2		breng	$⊢ (\emptyset \in V \land A \in V) \to (\emptyset \approx A \leftrightarrow \exists f f : \emptyset \underset{1-1 onto}{⟶} A)$
3	1 2	syl	$⊢ \emptyset \approx A \to (\emptyset \approx A \leftrightarrow \exists f f : \emptyset \underset{1-1 onto}{⟶} A)$
4	3	ibi	$⊢ \emptyset \approx A \to \exists f f : \emptyset \underset{1-1 onto}{⟶} A$
5		f1o00	$⊢ f : \emptyset \underset{1-1 onto}{⟶} A \leftrightarrow (f = \emptyset \land A = \emptyset)$
6	5	simprbi	$⊢ f : \emptyset \underset{1-1 onto}{⟶} A \to A = \emptyset$
7	6	exlimiv	$⊢ \exists f f : \emptyset \underset{1-1 onto}{⟶} A \to A = \emptyset$
8	4 7	syl	$⊢ \emptyset \approx A \to A = \emptyset$
9		0ex	$⊢ \emptyset \in V$
10		f1oeq1	$⊢ f = \emptyset \to (f : \emptyset \underset{1-1 onto}{⟶} \emptyset \leftrightarrow \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset)$
11		f1o0	$⊢ \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
12	9 10 11	ceqsexv2d	$⊢ \exists f f : \emptyset \underset{1-1 onto}{⟶} \emptyset$
13		breng	$⊢ (\emptyset \in V \land \emptyset \in V) \to (\emptyset \approx \emptyset \leftrightarrow \exists f f : \emptyset \underset{1-1 onto}{⟶} \emptyset)$
14	9 9 13	mp2an	$⊢ \emptyset \approx \emptyset \leftrightarrow \exists f f : \emptyset \underset{1-1 onto}{⟶} \emptyset$
15	12 14	mpbir	$⊢ \emptyset \approx \emptyset$
16		breq2	$⊢ A = \emptyset \to (\emptyset \approx A \leftrightarrow \emptyset \approx \emptyset)$
17	15 16	mpbiri	$⊢ A = \emptyset \to \emptyset \approx A$
18	8 17	impbii	$⊢ \emptyset \approx A \leftrightarrow A = \emptyset$