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