This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelopab4

Description: Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab . (Contributed by Alan Sare, 8-Feb-2014) (Revised by Mario Carneiro, 6-May-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion opelopab4 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 elopab ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ↔ ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
5 eqcom ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ↔ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
6 4 5 bitr3i ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ↔ ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
7 6 anbi1i ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
8 7 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
9 1 8 bitr4i ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )