Description: The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995) (Revised by David Abernethy, 19-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | nfoprab1 | |- F/_ x { <. <. 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/ x E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) |
|
3 | 2 | nfab | |- F/_ x { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) } |
4 | 1 3 | nfcxfr | |- F/_ x { <. <. x , y >. , z >. | ph } |