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

Theorem nfxp 5710
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 5683 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2891 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2891 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1903 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5218 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2902 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 397  wcel 2107  wnfc 2884  {copab 5211   × cxp 5675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-opab 5212  df-xp 5683
This theorem is referenced by:  opeliunxp  5744  nfres  5984  mpomptsx  8050  dmmpossx  8052  fmpox  8053  ovmptss  8079  nfdju  9902  axcc2  10432  fsum2dlem  15716  fsumcom2  15720  fprod2dlem  15924  fprodcom2  15928  gsumcom2  19843  prdsdsf  23873  prdsxmet  23875  djussxp2  31873  aciunf1lem  31887  gsumpart  32207  esum2dlem  33090  poimirlem16  36504  poimirlem19  36507  dvnprodlem1  44662  stoweidlem21  44737  stoweidlem47  44763  opeliun2xp  47008  dmmpossx2  47012
  Copyright terms: Public domain W3C validator