Metamath Proof Explorer


Theorem dfoprab3

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis dfoprab3.1 w=xyφψ
Assertion dfoprab3 wz|wV×Vφ=xyz|ψ

Proof

Step Hyp Ref Expression
1 dfoprab3.1 w=xyφψ
2 dfoprab3s xyz|ψ=wz|wV×V[˙1stw/x]˙[˙2ndw/y]˙ψ
3 fvex 1stwV
4 fvex 2ndwV
5 eqcom x=1stw1stw=x
6 eqcom y=2ndw2ndw=y
7 5 6 anbi12i x=1stwy=2ndw1stw=x2ndw=y
8 eqopi wV×V1stw=x2ndw=yw=xy
9 7 8 sylan2b wV×Vx=1stwy=2ndww=xy
10 9 1 syl wV×Vx=1stwy=2ndwφψ
11 10 bicomd wV×Vx=1stwy=2ndwψφ
12 11 ex wV×Vx=1stwy=2ndwψφ
13 3 4 12 sbc2iedv wV×V[˙1stw/x]˙[˙2ndw/y]˙ψφ
14 13 pm5.32i wV×V[˙1stw/x]˙[˙2ndw/y]˙ψwV×Vφ
15 14 opabbii wz|wV×V[˙1stw/x]˙[˙2ndw/y]˙ψ=wz|wV×Vφ
16 2 15 eqtr2i wz|wV×Vφ=xyz|ψ