Theorem nfxp 5016

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 4995	. 2 |- ( A X. B ) = { <. y , z >. | ( y e. A /\ z e. B ) }
2		nfxp.1	. . . . 5 |- F/_ x A
3	2	nfcri 2598	. . . 4 |- F/ x y e. A
4		nfxp.2	. . . . 5 |- F/_ x B
5	4	nfcri 2598	. . . 4 |- F/ x z e. B
6	3, 5	nfan 1914	. . 3 |- F/ x ( y e. A /\ z e. B )
7	6	nfopab 4502	. 2 |- F/_ x { <. y , z >. | ( y e. A /\ z e. B ) }
8	1, 7	nfcxfr 2603	1 |- F/_ x ( A X. B )

Syntax hints:   /\ wa 369   e. wcel 1804   F/_wnfc 2591   {copab 4494   X. cxp 4987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-opab 4496  df-xp 4995

This theorem is referenced by:  opeliunxp  5041  nfres  5265  mpt2mptsx  6848  dmmpt2ssx  6850  fmpt2x  6851  ovmptss  6866  axcc2  8820  fsum2dlem  13566  fsumcom2  13570  fprod2dlem  13765  fprodcom2  13769  gsumcom2  16981  prdsdsf  20847  prdsxmet  20849  stoweidlem21  31692  stoweidlem47  31718  opeliun2xp  32655  dmmpt2ssx2  32659