Theorem opeqex

Description: Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008)

	Ref	Expression
Assertion	opeqex	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) )

Proof

Step	Hyp	Ref	Expression
1		neeq1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ ↔ ⟨ 𝐶 , 𝐷 ⟩ ≠ ∅ ) )
2		opnz	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3		opnz	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ≠ ∅ ↔ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
4	1 2 3	3bitr3g	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) )