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

Theorem nfxp 4731
Description: Bound-variable hypothesis builder for cross 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 4711 . 2  |-  ( A  X.  B )  =  { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
2 nfxp.1 . . . . 5  |-  F/_ x A
32nfcri 2426 . . . 4  |-  F/ x  y  e.  A
4 nfxp.2 . . . . 5  |-  F/_ x B
54nfcri 2426 . . . 4  |-  F/ x  z  e.  B
63, 5nfan 1783 . . 3  |-  F/ x
( y  e.  A  /\  z  e.  B
)
76nfopab 4100 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
81, 7nfcxfr 2429 1  |-  F/_ x
( A  X.  B
)
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1696   F/_wnfc 2419   {copab 4092    X. cxp 4703
This theorem is referenced by:  opeliunxp  4756  nfres  4973  mpt2mptsx  6203  dmmpt2ssx  6205  fmpt2x  6206  ovmptss  6216  axcc2  8079  fsum2dlem  12249  fsumcom2  12253  gsumcom2  15242  prdsdsf  17947  prdsxmet  17949  dya2iocrrnval  23597  stoweidlem21  27873  stoweidlem47  27899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-opab 4094  df-xp 4711
  Copyright terms: Public domain W3C validator