Description: The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995) (Revised by David Abernethy, 30-Jul-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | nfoprab2 | |- F/_ y { <. <. x , y >. , z >. | ph } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-oprab | |- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) } |
|
2 | nfe1 | |- F/ y E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) |
|
3 | 2 | nfex | |- F/ y E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) |
4 | 3 | nfab | |- F/_ y { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) } |
5 | 1 4 | nfcxfr | |- F/_ y { <. <. x , y >. , z >. | ph } |