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

Theorem nfxp 5671
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 5644 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2895 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2895 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1903 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5179 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2906 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 397  wcel 2107  wnfc 2888  {copab 5172   × cxp 5636
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-opab 5173  df-xp 5644
This theorem is referenced by:  opeliunxp  5704  nfres  5944  mpomptsx  8001  dmmpossx  8003  fmpox  8004  ovmptss  8030  nfdju  9850  axcc2  10380  fsum2dlem  15662  fsumcom2  15666  fprod2dlem  15870  fprodcom2  15874  gsumcom2  19759  prdsdsf  23736  prdsxmet  23738  djussxp2  31606  aciunf1lem  31620  gsumpart  31939  esum2dlem  32731  poimirlem16  36123  poimirlem19  36126  dvnprodlem1  44261  stoweidlem21  44336  stoweidlem47  44362  opeliun2xp  46482  dmmpossx2  46486
  Copyright terms: Public domain W3C validator