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

Theorem nfxp 5556
 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 5529 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2943 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2943 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1900 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5102 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2953 1 𝑥(𝐴 × 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   ∈ wcel 2111  Ⅎwnfc 2936  {copab 5096   × cxp 5521 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-opab 5097  df-xp 5529 This theorem is referenced by:  opeliunxp  5587  nfres  5824  mpomptsx  7757  dmmpossx  7759  fmpox  7760  ovmptss  7784  nfdju  9338  axcc2  9866  fsum2dlem  15137  fsumcom2  15141  fprod2dlem  15346  fprodcom2  15350  gsumcom2  19109  prdsdsf  23015  prdsxmet  23017  djussxp2  30454  aciunf1lem  30469  gsumpart  30789  esum2dlem  31527  poimirlem16  35224  poimirlem19  35227  dvnprodlem1  42756  stoweidlem21  42831  stoweidlem47  42857  opeliun2xp  44902  dmmpossx2  44906
 Copyright terms: Public domain W3C validator