pren2

Description: An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023)

		Ref	Expression
	Assertion	pren2	$⊢ \{A, B\} \approx 2_{𝑜} \leftrightarrow (A \in V \land B \in V \land A \neq B)$

Step	Hyp	Ref	Expression
1		pr2ne	$⊢ (A \in V \land B \in V) \to (\{A, B\} \approx 2_{𝑜} \leftrightarrow A \neq B)$
2	1	pm5.32i	$⊢ ((A \in V \land B \in V) \land \{A, B\} \approx 2_{𝑜}) \leftrightarrow ((A \in V \land B \in V) \land A \neq B)$
3		pr2cv	$⊢ \{A, B\} \approx 2_{𝑜} \to (A \in V \land B \in V)$
4	3	pm4.71ri	$⊢ \{A, B\} \approx 2_{𝑜} \leftrightarrow ((A \in V \land B \in V) \land \{A, B\} \approx 2_{𝑜})$
5		df-3an	$⊢ (A \in V \land B \in V \land A \neq B) \leftrightarrow ((A \in V \land B \in V) \land A \neq B)$
6	2 4 5	3bitr4i	$⊢ \{A, B\} \approx 2_{𝑜} \leftrightarrow (A \in V \land B \in V \land A \neq B)$

Metamath Proof Explorer