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 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) }