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

Theorem nfxp 5714
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 5687 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2882 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2882 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1894 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 5221 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2889 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 394  wcel 2098  wnfc 2875  {copab 5214   × cxp 5679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-opab 5215  df-xp 5687
This theorem is referenced by:  opeliunxp  5748  nfres  5990  mpomptsx  8077  dmmpossx  8079  fmpox  8080  ovmptss  8106  nfdju  9946  axcc2  10476  fsum2dlem  15769  fsumcom2  15773  fprod2dlem  15977  fprodcom2  15981  gsumcom2  19968  prdsdsf  24356  prdsxmet  24358  djussxp2  32556  aciunf1lem  32570  gsumpart  32901  esum2dlem  33881  poimirlem16  37285  poimirlem19  37288  dvnprodlem1  45504  stoweidlem21  45579  stoweidlem47  45605  opeliun2xp  47648  dmmpossx2  47652
  Copyright terms: Public domain W3C validator