Theorem altopthc

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

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

Proof

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