MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfxp Structured version   Visualization version   GIF version

Theorem nfxp 5584
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.
StepHypRef Expression
1 df-xp 5557 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2891 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2891 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1907 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5122 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2902 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 399  wcel 2110  wnfc 2884  {copab 5115   × cxp 5549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-opab 5116  df-xp 5557
This theorem is referenced by:  opeliunxp  5616  nfres  5853  mpomptsx  7834  dmmpossx  7836  fmpox  7837  ovmptss  7861  nfdju  9523  axcc2  10051  fsum2dlem  15334  fsumcom2  15338  fprod2dlem  15542  fprodcom2  15546  gsumcom2  19360  prdsdsf  23265  prdsxmet  23267  djussxp2  30704  aciunf1lem  30719  gsumpart  31034  esum2dlem  31772  poimirlem16  35530  poimirlem19  35533  dvnprodlem1  43162  stoweidlem21  43237  stoweidlem47  43263  opeliun2xp  45341  dmmpossx2  45345
  Copyright terms: Public domain W3C validator