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

Theorem nfxp 5708
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 5681 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2890 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2890 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1902 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5216 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2901 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2106  wnfc 2883  {copab 5209   × cxp 5673
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-opab 5210  df-xp 5681
This theorem is referenced by:  opeliunxp  5741  nfres  5981  mpomptsx  8046  dmmpossx  8048  fmpox  8049  ovmptss  8075  nfdju  9898  axcc2  10428  fsum2dlem  15712  fsumcom2  15716  fprod2dlem  15920  fprodcom2  15924  gsumcom2  19837  prdsdsf  23864  prdsxmet  23866  djussxp2  31860  aciunf1lem  31874  gsumpart  32194  esum2dlem  33078  poimirlem16  36492  poimirlem19  36495  dvnprodlem1  44648  stoweidlem21  44723  stoweidlem47  44749  opeliun2xp  46961  dmmpossx2  46965
  Copyright terms: Public domain W3C validator