Theorem pren2d

Description: A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023)

	Ref	Expression
Hypotheses	pren2d.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	pren2d.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	pren2d.aneb	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	pren2d	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )

Proof

Step	Hyp	Ref	Expression
1		pren2d.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		pren2d.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		pren2d.aneb	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
4	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
5	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
6		pren2	⊢ ( { 𝐴 , 𝐵 } ≈ 2o ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) )
7	4 5 3 6	syl3anbrc	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )