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

Theorem nfxp 5031
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 5010 . 2
2 nfxp.1 . . . . 5
32nfcri 2612 . . . 4
4 nfxp.2 . . . . 5
54nfcri 2612 . . . 4
63, 5nfan 1928 . . 3
76nfopab 4517 . 2
81, 7nfcxfr 2617 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  e.wcel 1818  F/_wnfc 2605  {copab 4509  X.cxp 5002
This theorem is referenced by:  opeliunxp  5056  nfres  5280  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  ovmptss  6881  axcc2  8838  fsum2dlem  13585  fsumcom2  13589  fprod2dlem  13784  fprodcom2  13788  gsumcom2  17003  prdsdsf  20870  prdsxmet  20872  dvnprodlem1  31743  stoweidlem21  31803  stoweidlem47  31829  opeliun2xp  32922  dmmpt2ssx2  32926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator