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

Metamath Proof Explorer

Theorem dfoprab3s

Description: A way to define an operation class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dfoprab3s { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) }

Proof

Step Hyp Ref Expression
1 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
2 nfsbc1v ⊢ Ⅎ 𝑥 [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑
3 2 19.41 ⊢ ( ∃ 𝑥 ( ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
4 sbcopeq1a ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ↔ 𝜑 ) )
5 4 pm5.32i ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
7 nfcv ⊢ Ⅎ 𝑦 ( 1st ‘ 𝑤 )
8 nfsbc1v ⊢ Ⅎ 𝑦 [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑
9 7 8 nfsbcw ⊢ Ⅎ 𝑦 [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑
10 9 19.41 ⊢ ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
11 6 10 bitr3i ⊢ ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
12 11 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
13 elvv ⊢ ( 𝑤 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
14 13 anbi1i ⊢ ( ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
15 3 12 14 3bitr4i ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
16 15 opabbii ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) }
17 1 16 eqtri ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ [ ( 1st ‘ 𝑤 ) / 𝑥 ] [ ( 2nd ‘ 𝑤 ) / 𝑦 ] 𝜑 ) }