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

Theorem nfxp 5722
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 5695 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2895 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2895 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1897 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5217 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2901 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 395  wcel 2106  wnfc 2888  {copab 5210   × cxp 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-opab 5211  df-xp 5695
This theorem is referenced by:  opeliunxp  5756  nfres  6002  mpomptsx  8088  dmmpossx  8090  fmpox  8091  ovmptss  8117  nfdju  9945  axcc2  10475  fsum2dlem  15803  fsumcom2  15807  fprod2dlem  16013  fprodcom2  16017  gsumcom2  20008  prdsdsf  24393  prdsxmet  24395  djussxp2  32665  aciunf1lem  32679  gsumpart  33043  esum2dlem  34073  poimirlem16  37623  poimirlem19  37626  dvnprodlem1  45902  stoweidlem21  45977  stoweidlem47  46003  opeliun2xp  48178  dmmpossx2  48182
  Copyright terms: Public domain W3C validator