Theorem altopth

Description: The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that C and D are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth ), requires D to be a set. (Contributed by Scott Fenton, 23-Mar-2012)

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

Proof

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