Metamath Proof Explorer

Theorem enpr2

Description: An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d . (Contributed by FL, 17-Aug-2008) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 30-Dec-2024)

		Ref	Expression
	Assertion	enpr2	$⊢ (A \in C \land B \in D \land A \neq B) \to \{A, B\} \approx 2_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
2		simp1	$⊢ (A \in C \land B \in D \land \neg A = B) \to A \in C$
3		simp2	$⊢ (A \in C \land B \in D \land \neg A = B) \to B \in D$
4		simp3	$⊢ (A \in C \land B \in D \land \neg A = B) \to \neg A = B$
5	2 3 4	enpr2d	$⊢ (A \in C \land B \in D \land \neg A = B) \to \{A, B\} \approx 2_{𝑜}$
6	1 5	syl3an3b	$⊢ (A \in C \land B \in D \land A \neq B) \to \{A, B\} \approx 2_{𝑜}$