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 _xxAB

Proof

Step Hyp Ref Expression
1 df-ixp xAB=y|yFnx|xAxAyxB
2 nfcv _xy
3 nfab1 _xx|xA
4 2 3 nffn xyFnx|xA
5 nfra1 xxAyxB
6 4 5 nfan xyFnx|xAxAyxB
7 6 nfab _xy|yFnx|xAxAyxB
8 1 7 nfcxfr _xxAB