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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-oprab | ||
2 | nfe1 | ||
3 | 2 | nfex | |
4 | 3 | nfab | |
5 | 1 4 | nfcxfr |