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

Metamath Proof Explorer

Theorem vopelopabsb

Description: The law of concretion in terms of substitutions. Version of opelopabsb with set variables. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) Remove unnecessary commutation. (Revised by SN, 1-Sep-2024)

Ref Expression
Assertion vopelopabsb ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 eqcom ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
5 1 4 bitri ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
6 5 anbi1i ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) )
7 6 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) )
8 elopab ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
9 2sb5 ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) )
10 7 8 9 3bitr4i ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )