Theorem altopthd

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

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

Proof

Step	Hyp	Ref	Expression
1		altopthd.1	⊢ 𝐶 ∈ V
2		altopthd.2	⊢ 𝐷 ∈ V
3		eqcom	⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ⟪ 𝐶 , 𝐷 ⟫ = ⟪ 𝐴 , 𝐵 ⟫ )
4	1 2	altopth	⊢ ( ⟪ 𝐶 , 𝐷 ⟫ = ⟪ 𝐴 , 𝐵 ⟫ ↔ ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) )
5		eqcom	⊢ ( 𝐶 = 𝐴 ↔ 𝐴 = 𝐶 )
6		eqcom	⊢ ( 𝐷 = 𝐵 ↔ 𝐵 = 𝐷 )
7	5 6	anbi12i	⊢ ( ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
8	3 4 7	3bitri	⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )