Metamath Proof Explorer


Theorem oprabrexex2

Description: Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010)

Ref Expression
Hypotheses oprabrexex2.1
|- A e. _V
oprabrexex2.2
|- { <. <. x , y >. , z >. | ph } e. _V
Assertion oprabrexex2
|- { <. <. x , y >. , z >. | E. w e. A ph } e. _V

Proof

Step Hyp Ref Expression
1 oprabrexex2.1
 |-  A e. _V
2 oprabrexex2.2
 |-  { <. <. x , y >. , z >. | ph } e. _V
3 df-oprab
 |-  { <. <. x , y >. , z >. | E. w e. A ph } = { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) }
4 rexcom4
 |-  ( E. w e. A E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. x E. w e. A E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) )
5 rexcom4
 |-  ( E. w e. A E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. y E. w e. A E. z ( v = <. <. x , y >. , z >. /\ ph ) )
6 rexcom4
 |-  ( E. w e. A E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. z E. w e. A ( v = <. <. x , y >. , z >. /\ ph ) )
7 r19.42v
 |-  ( E. w e. A ( v = <. <. x , y >. , z >. /\ ph ) <-> ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) )
8 7 exbii
 |-  ( E. z E. w e. A ( v = <. <. x , y >. , z >. /\ ph ) <-> E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) )
9 6 8 bitri
 |-  ( E. w e. A E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) )
10 9 exbii
 |-  ( E. y E. w e. A E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. y E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) )
11 5 10 bitri
 |-  ( E. w e. A E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. y E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) )
12 11 exbii
 |-  ( E. x E. w e. A E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. x E. y E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) )
13 4 12 bitr2i
 |-  ( E. x E. y E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) <-> E. w e. A E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) )
14 13 abbii
 |-  { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ E. w e. A ph ) } = { v | E. w e. A E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
15 3 14 eqtri
 |-  { <. <. x , y >. , z >. | E. w e. A ph } = { v | E. w e. A E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
16 df-oprab
 |-  { <. <. x , y >. , z >. | ph } = { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
17 16 2 eqeltrri
 |-  { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) } e. _V
18 1 17 abrexex2
 |-  { v | E. w e. A E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) } e. _V
19 15 18 eqeltri
 |-  { <. <. x , y >. , z >. | E. w e. A ph } e. _V