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

Metamath Proof Explorer

Theorem dfoprab3

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis dfoprab3.1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion dfoprab3 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }

Proof

Step Hyp Ref Expression
1 dfoprab3.1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2 dfoprab3s ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜓 ) }
3 fvex ⊢ ( 1st ‘ 𝑤 ) ∈ V
4 fvex ⊢ ( 2nd ‘ 𝑤 ) ∈ V
5 eqcom ⊢ ( 𝑥 = ( 1st ‘ 𝑤 ) ↔ ( 1st ‘ 𝑤 ) = 𝑥 )
6 eqcom ⊢ ( 𝑦 = ( 2nd ‘ 𝑤 ) ↔ ( 2nd ‘ 𝑤 ) = 𝑦 )
7 5 6 anbi12i ⊢ ( ( 𝑥 = ( 1st ‘ 𝑤 ) ∧ 𝑦 = ( 2nd ‘ 𝑤 ) ) ↔ ( ( 1st ‘ 𝑤 ) = 𝑥 ∧ ( 2nd ‘ 𝑤 ) = 𝑦 ) )
8 eqopi ⊢ ( ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) = 𝑥 ∧ ( 2nd ‘ 𝑤 ) = 𝑦 ) ) → 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
9 7 8 sylan2b ⊢ ( ( 𝑤 ∈ ( V × V ) ∧ ( 𝑥 = ( 1st ‘ 𝑤 ) ∧ 𝑦 = ( 2nd ‘ 𝑤 ) ) ) → 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
10 9 1 syl ⊢ ( ( 𝑤 ∈ ( V × V ) ∧ ( 𝑥 = ( 1st ‘ 𝑤 ) ∧ 𝑦 = ( 2nd ‘ 𝑤 ) ) ) → ( 𝜑 ↔ 𝜓 ) )
11 10 bicomd ⊢ ( ( 𝑤 ∈ ( V × V ) ∧ ( 𝑥 = ( 1st ‘ 𝑤 ) ∧ 𝑦 = ( 2nd ‘ 𝑤 ) ) ) → ( 𝜓 ↔ 𝜑 ) )
12 11 ex ⊢ ( 𝑤 ∈ ( V × V ) → ( ( 𝑥 = ( 1st ‘ 𝑤 ) ∧ 𝑦 = ( 2nd ‘ 𝑤 ) ) → ( 𝜓 ↔ 𝜑 ) ) )
13 3 4 12 sbc2iedv ⊢ ( 𝑤 ∈ ( V × V ) → ( [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜓 ↔ 𝜑 ) )
14 13 pm5.32i ⊢ ( ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜓 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ 𝜑 ) )
15 14 opabbii ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜓 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝜑 ) }
16 2 15 eqtr2i ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }