Theorem nfxp 5657

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	⊢ Ⅎ𝑥𝐴
nfxp.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfxp	⊢ Ⅎ𝑥(𝐴 × 𝐵)

Proof of Theorem nfxp

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-xp 5630	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2		nfxp.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2891	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfxp.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2891	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵
6	3, 5	nfan 1901	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)
7	6	nfopab 5155	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
8	1, 7	nfcxfr 2897	1 ⊢ Ⅎ𝑥(𝐴 × 𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2114  Ⅎwnfc 2884  {copab 5148   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-opab 5149  df-xp 5630

This theorem is referenced by:  opeliunxp  5691  opeliun2xp  5692  nfres  5940  mpomptsx  8010  dmmpossx  8012  fmpox  8013  ovmptss  8036  nfdju  9822  axcc2  10350  fsum2dlem  15723  fsumcom2  15727  fprod2dlem  15936  fprodcom2  15940  gsumcom2  19941  prdsdsf  24342  prdsxmet  24344  iunxpssiun1  32653  djussxp2  32736  aciunf1lem  32750  gsumpart  33139  esum2dlem  34252  poimirlem16  37971  poimirlem19  37974  dvnprodlem1  46392  stoweidlem21  46467  stoweidlem47  46493  dmmpossx2  48825