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 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }