Theorem nfxp 4879

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

Hypotheses

Ref	Expression
nfxp.1	|- F/_ x A
nfxp.2	|- F/_ x B

Assertion

Ref	Expression
nfxp	|- F/_ x ( A X. B )

Proof of Theorem nfxp

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-xp 4858	. 2 |- ( A X. B ) = { <. y , z >. | ( y e. A /\ z e. B ) }
2		nfxp.1	. . . . 5 |- F/_ x A
3	2	nfcri 2596	. . . 4 |- F/ x y e. A
4		nfxp.2	. . . . 5 |- F/_ x B
5	4	nfcri 2596	. . . 4 |- F/ x z e. B
6	3, 5	nfan 2021	. . 3 |- F/ x ( y e. A /\ z e. B )
7	6	nfopab 4481	. 2 |- F/_ x { <. y , z >. | ( y e. A /\ z e. B ) }
8	1, 7	nfcxfr 2600	1 |- F/_ x ( A X. B )

Syntax hints:   /\ wa 375   e. wcel 1897   F/_wnfc 2589   {copab 4473   X. cxp 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-opab 4475  df-xp 4858

This theorem is referenced by:  opeliunxp  4904  nfres  5125  mpt2mptsx  6882  dmmpt2ssx  6884  fmpt2x  6885  ovmptss  6903  axcc2  8892  fsum2dlem  13879  fsumcom2  13883  fprod2dlem  14082  fprodcom2  14086  gsumcom2  17655  prdsdsf  21430  prdsxmet  21432  aciunf1lem  28312  esum2dlem  28961  poimirlem16  32000  poimirlem19  32003  dvnprodlem1  37858  stoweidlem21  37918  stoweidlem47  37945  opeliun2xp  40386  dmmpt2ssx2  40390