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

Theorem nfxp 5032
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 5011 . 2  |-  ( A  X.  B )  =  { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
2 nfxp.1 . . . . 5  |-  F/_ x A
32nfcri 2622 . . . 4  |-  F/ x  y  e.  A
4 nfxp.2 . . . . 5  |-  F/_ x B
54nfcri 2622 . . . 4  |-  F/ x  z  e.  B
63, 5nfan 1875 . . 3  |-  F/ x
( y  e.  A  /\  z  e.  B
)
76nfopab 4518 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
81, 7nfcxfr 2627 1  |-  F/_ x
( A  X.  B
)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1767   F/_wnfc 2615   {copab 4510    X. cxp 5003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-opab 4512  df-xp 5011
This theorem is referenced by:  opeliunxp  5057  nfres  5281  mpt2mptsx  6858  dmmpt2ssx  6860  fmpt2x  6861  ovmptss  6876  axcc2  8829  fsum2dlem  13565  fsumcom2  13569  gsumcom2  16876  prdsdsf  20738  prdsxmet  20740  fprod2dlem  29037  fprodcom2  29041  stoweidlem21  31644  stoweidlem47  31670  opeliun2xp  32401  dmmpt2ssx2  32405
  Copyright terms: Public domain W3C validator