Description: The first abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 14-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfopab1 | |- F/_ x { <. x , y >. | ph } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-opab | |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) } |
|
| 2 | nfe1 | |- F/ x E. x E. y ( z = <. x , y >. /\ ph ) |
|
| 3 | 2 | nfab | |- F/_ x { z | E. x E. y ( z = <. x , y >. /\ ph ) } |
| 4 | 1 3 | nfcxfr | |- F/_ x { <. x , y >. | ph } |