Theorem nfxp 5032

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 5011	. 2 |- ( A X. B ) = { <. y , z >. | ( y e. A /\ z e. B ) }
2		nfxp.1	. . . . 5 |- F/_ x A
3	2	nfcri 2622	. . . 4 |- F/ x y e. A
4		nfxp.2	. . . . 5 |- F/_ x B
5	4	nfcri 2622	. . . 4 |- F/ x z e. B
6	3, 5	nfan 1875	. . 3 |- F/ x ( y e. A /\ z e. B )
7	6	nfopab 4518	. 2 |- F/_ x { <. y , z >. | ( y e. A /\ z e. B ) }
8	1, 7	nfcxfr 2627	1 |- F/_ x ( A X. B )

Syntax hints:   /\ wa 369   e. wcel 1767   F/_wnfc 2615   {copab 4510   X. cxp 5003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-opab 4512  df-xp 5011

This theorem is referenced by:  opeliunxp  5057  nfres  5281  mpt2mptsx  6858  dmmpt2ssx  6860  fmpt2x  6861  ovmptss  6876  axcc2  8829  fsum2dlem  13565  fsumcom2  13569  gsumcom2  16876  prdsdsf  20738  prdsxmet  20740  fprod2dlem  29037  fprodcom2  29041  stoweidlem21  31644  stoweidlem47  31670  opeliun2xp  32401  dmmpt2ssx2  32405