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

Theorem nfxp 4879
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  |-  F/_ x A
nfxp.2  |-  F/_ x B
Assertion
Ref Expression
nfxp  |-  F/_ x
( A  X.  B
)

Proof of Theorem nfxp
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-xp 4858 . 2  |-  ( A  X.  B )  =  { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
2 nfxp.1 . . . . 5  |-  F/_ x A
32nfcri 2596 . . . 4  |-  F/ x  y  e.  A
4 nfxp.2 . . . . 5  |-  F/_ x B
54nfcri 2596 . . . 4  |-  F/ x  z  e.  B
63, 5nfan 2021 . . 3  |-  F/ x
( y  e.  A  /\  z  e.  B
)
76nfopab 4481 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
81, 7nfcxfr 2600 1  |-  F/_ x
( A  X.  B
)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 375    e. wcel 1897   F/_wnfc 2589   {copab 4473    X. cxp 4850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-opab 4475  df-xp 4858
This theorem is referenced by:  opeliunxp  4904  nfres  5125  mpt2mptsx  6882  dmmpt2ssx  6884  fmpt2x  6885  ovmptss  6903  axcc2  8892  fsum2dlem  13879  fsumcom2  13883  fprod2dlem  14082  fprodcom2  14086  gsumcom2  17655  prdsdsf  21430  prdsxmet  21432  aciunf1lem  28312  esum2dlem  28961  poimirlem16  32000  poimirlem19  32003  dvnprodlem1  37858  stoweidlem21  37918  stoweidlem47  37945  opeliun2xp  40386  dmmpt2ssx2  40390
  Copyright terms: Public domain W3C validator