Metamath Proof Explorer


Theorem nfxp

Description: Bound-variable hypothesis builder for Cartesian product. (Contributed by NM, 15-Sep-2003) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses nfxp.1 _ x A
nfxp.2 _ x B
Assertion nfxp _ x A × B

Proof

Step Hyp Ref Expression
1 nfxp.1 _ x A
2 nfxp.2 _ x B
3 df-xp A × B = y z | y A z B
4 1 nfcri x y A
5 2 nfcri x z B
6 4 5 nfan x y A z B
7 6 nfopab _ x y z | y A z B
8 3 7 nfcxfr _ x A × B