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