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

Theorem nfxp 4715
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 4695 . 2  |-  ( A  X.  B )  =  { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
2 nfxp.1 . . . . 5  |-  F/_ x A
32nfcri 2413 . . . 4  |-  F/ x  y  e.  A
4 nfxp.2 . . . . 5  |-  F/_ x B
54nfcri 2413 . . . 4  |-  F/ x  z  e.  B
63, 5nfan 1771 . . 3  |-  F/ x
( y  e.  A  /\  z  e.  B
)
76nfopab 4084 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
81, 7nfcxfr 2416 1  |-  F/_ x
( A  X.  B
)
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1684   F/_wnfc 2406   {copab 4076    X. cxp 4687
This theorem is referenced by:  opeliunxp  4740  nfres  4957  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  ovmptss  6200  axcc2  8063  fsum2dlem  12233  fsumcom2  12237  gsumcom2  15226  prdsdsf  17931  prdsxmet  17933  dya2iocrrnval  23582  stoweidlem21  27770  stoweidlem47  27796
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-opab 4078  df-xp 4695
  Copyright terms: Public domain W3C validator