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 |