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

Theorem nfxp 5016
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 4995 . 2  |-  ( A  X.  B )  =  { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
2 nfxp.1 . . . . 5  |-  F/_ x A
32nfcri 2598 . . . 4  |-  F/ x  y  e.  A
4 nfxp.2 . . . . 5  |-  F/_ x B
54nfcri 2598 . . . 4  |-  F/ x  z  e.  B
63, 5nfan 1914 . . 3  |-  F/ x
( y  e.  A  /\  z  e.  B
)
76nfopab 4502 . 2  |-  F/_ x { <. y ,  z
>.  |  ( y  e.  A  /\  z  e.  B ) }
81, 7nfcxfr 2603 1  |-  F/_ x
( A  X.  B
)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1804   F/_wnfc 2591   {copab 4494    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-opab 4496  df-xp 4995
This theorem is referenced by:  opeliunxp  5041  nfres  5265  mpt2mptsx  6848  dmmpt2ssx  6850  fmpt2x  6851  ovmptss  6866  axcc2  8820  fsum2dlem  13566  fsumcom2  13570  fprod2dlem  13765  fprodcom2  13769  gsumcom2  16981  prdsdsf  20847  prdsxmet  20849  stoweidlem21  31692  stoweidlem47  31718  opeliun2xp  32655  dmmpt2ssx2  32659
  Copyright terms: Public domain W3C validator