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

Metamath Proof Explorer

Theorem enpr2d

Description: A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023) Avoid ax-un . (Revised by BTernaryTau, 23-Dec-2024)

		Ref	Expression
	Hypotheses	enpr2d.1	$⊢ φ \to A \in C$
		enpr2d.2	$⊢ φ \to B \in D$
		enpr2d.3	$⊢ φ \to \neg A = B$
	Assertion	enpr2d	$⊢ φ \to \{A, B\} \approx 2_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		enpr2d.1	$⊢ φ \to A \in C$
2		enpr2d.2	$⊢ φ \to B \in D$
3		enpr2d.3	$⊢ φ \to \neg A = B$
4		0ex	$⊢ \emptyset \in V$
5	4	a1i	$⊢ φ \to \emptyset \in V$
6		1oex	$⊢ 1_{𝑜} \in V$
7	6	a1i	$⊢ φ \to 1_{𝑜} \in V$
8	3	neqned	$⊢ φ \to A \neq B$
9		1n0	$⊢ 1_{𝑜} \neq \emptyset$
10	9	necomi	$⊢ \emptyset \neq 1_{𝑜}$
11	10	a1i	$⊢ φ \to \emptyset \neq 1_{𝑜}$
12	1 2 5 7 8 11	en2prd	$⊢ φ \to \{A, B\} \approx \{\emptyset, 1_{𝑜}\}$
13		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
14	12 13	breqtrrdi	$⊢ φ \to \{A, B\} \approx 2_{𝑜}$