Theorem nfxp 5733

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 5706	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2		nfxp.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2900	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfxp.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2900	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵
6	3, 5	nfan 1898	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)
7	6	nfopab 5235	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
8	1, 7	nfcxfr 2906	1 ⊢ Ⅎ𝑥(𝐴 × 𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2108  Ⅎwnfc 2893  {copab 5228   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-opab 5229  df-xp 5706

This theorem is referenced by:  opeliunxp  5767  nfres  6011  mpomptsx  8105  dmmpossx  8107  fmpox  8108  ovmptss  8134  nfdju  9976  axcc2  10506  fsum2dlem  15818  fsumcom2  15822  fprod2dlem  16028  fprodcom2  16032  gsumcom2  20017  prdsdsf  24398  prdsxmet  24400  djussxp2  32666  aciunf1lem  32680  gsumpart  33038  esum2dlem  34056  poimirlem16  37596  poimirlem19  37599  dvnprodlem1  45867  stoweidlem21  45942  stoweidlem47  45968  opeliun2xp  48057  dmmpossx2  48061