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

Metamath Proof Explorer

Theorem dfopab2

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

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

Proof

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