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 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥𝑦 ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) ∧ 𝜑 ) )