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

Theorem nfxp 5581
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 5554 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2968 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2968 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1891 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5125 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2972 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  wnfc 2958  {copab 5119   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-opab 5120  df-xp 5554
This theorem is referenced by:  opeliunxp  5612  nfres  5848  mpomptsx  7751  dmmpossx  7753  fmpox  7754  ovmptss  7777  nfdju  9324  axcc2  9847  fsum2dlem  15113  fsumcom2  15117  fprod2dlem  15322  fprodcom2  15326  gsumcom2  19024  prdsdsf  22904  prdsxmet  22906  aciunf1lem  30335  esum2dlem  31250  poimirlem16  34789  poimirlem19  34792  dvnprodlem1  42107  stoweidlem21  42183  stoweidlem47  42209  opeliun2xp  44309  dmmpossx2  44313
  Copyright terms: Public domain W3C validator