Metamath Proof Explorer


Theorem nfixp1

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

Proof

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