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

Metamath Proof Explorer

Theorem nfoprab

Description: Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013)

Ref Expression
Hypothesis nfoprab.1 
|- F/ w ph
Assertion nfoprab 
|- F/_ w { <. <. x , y >. , z >. | ph }

Proof

Step Hyp Ref Expression
1 nfoprab.1 
 |-  F/ w ph
2 df-oprab 
 |-  { <. <. x , y >. , z >. | ph } = { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
3 nfv 
 |-  F/ w v = <. <. x , y >. , z >.
4 3 1 nfan 
 |-  F/ w ( v = <. <. x , y >. , z >. /\ ph )
5 4 nfex 
 |-  F/ w E. z ( v = <. <. x , y >. , z >. /\ ph )
6 5 nfex 
 |-  F/ w E. y E. z ( v = <. <. x , y >. , z >. /\ ph )
7 6 nfex 
 |-  F/ w E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph )
8 7 nfab 
 |-  F/_ w { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
9 2 8 nfcxfr 
 |-  F/_ w { <. <. x , y >. , z >. | ph }