Description: The index variable in an indexed Cartesian product is not free. (Contributed by Jeff Madsen, 19-Jun-2011) (Revised by Mario Carneiro, 15-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfixp1 | |- F/_ x X_ x e. A B |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ixp | |- X_ x e. A B = { y | ( y Fn { x | x e. A } /\ A. x e. A ( y ` x ) e. B ) } |
|
| 2 | nfcv | |- F/_ x y |
|
| 3 | nfab1 | |- F/_ x { x | x e. A } |
|
| 4 | 2 3 | nffn | |- F/ x y Fn { x | x e. A } |
| 5 | nfra1 | |- F/ x A. x e. A ( y ` x ) e. B |
|
| 6 | 4 5 | nfan | |- F/ x ( y Fn { x | x e. A } /\ A. x e. A ( y ` x ) e. B ) |
| 7 | 6 | nfab | |- F/_ x { y | ( y Fn { x | x e. A } /\ A. x e. A ( y ` x ) e. B ) } |
| 8 | 1 7 | nfcxfr | |- F/_ x X_ x e. A B |