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

Theorem nfxp 5444
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 5417 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2928 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2928 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1863 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5002 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2932 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 387  wcel 2051  wnfc 2918  {copab 4996   × cxp 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-opab 4997  df-xp 5417
This theorem is referenced by:  opeliunxp  5473  nfres  5702  mpomptsx  7576  dmmpossx  7578  fmpox  7579  ovmptss  7602  nfdju  9136  axcc2  9663  fsum2dlem  14991  fsumcom2  14995  fprod2dlem  15200  fprodcom2  15204  gsumcom2  18860  prdsdsf  22695  prdsxmet  22697  aciunf1lem  30186  esum2dlem  31027  poimirlem16  34389  poimirlem19  34392  dvnprodlem1  41696  stoweidlem21  41772  stoweidlem47  41798  opeliun2xp  43780  dmmpossx2  43784
  Copyright terms: Public domain W3C validator