This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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