Theorem altopthb

Description: Alternate ordered pair theorem with different sethood requirements. See altopth for more comments. (Contributed by Scott Fenton, 14-Apr-2012)

	Ref	Expression
Hypotheses	altopthb.1	⊢ 𝐴 ∈ V
	altopthb.2	⊢ 𝐷 ∈ V
Assertion	altopthb	⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		altopthb.1	⊢ 𝐴 ∈ V
2		altopthb.2	⊢ 𝐷 ∈ V
3		altopthbg	⊢ ( ( 𝐴 ∈ V ∧ 𝐷 ∈ V ) → ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
4	1 2 3	mp2an	⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )