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

Theorem nfrex 2611
Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfrex.1  |-  F/_ x A
nfrex.2  |-  F/ x ph
Assertion
Ref Expression
nfrex  |-  F/ x E. y  e.  A  ph

Proof of Theorem nfrex
StepHypRef Expression
1 dfrex2 2569 . 2  |-  ( E. y  e.  A  ph  <->  -. 
A. y  e.  A  -.  ph )
2 nfrex.1 . . . 4  |-  F/_ x A
3 nfrex.2 . . . . 5  |-  F/ x ph
43nfn 1777 . . . 4  |-  F/ x  -.  ph
52, 4nfral 2609 . . 3  |-  F/ x A. y  e.  A  -.  ph
65nfn 1777 . 2  |-  F/ x  -.  A. y  e.  A  -.  ph
71, 6nfxfr 1560 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1534   F/_wnfc 2419   A.wral 2556   E.wrex 2557
This theorem is referenced by:  r19.12  2669  sbcrexg  3079  nfuni  3849  nfiun  3947  nffr  4383  abrexex2g  5784  abrexex2  5796  nfrecs  6406  indexfi  7179  nfoi  7245  ixpiunwdom  7321  hsmexlem2  8069  iunfo  8177  iundom2g  8178  reclem2pr  8688  nfwrd  11442  nfsum1  12179  nfsum  12180  ptclsg  17325  iunmbl2  18930  mbfsup  19035  limciun  19260  xrofsup  23270  iundisjf  23380  nfcprod1  24132  nfcprod  24133  nfprod1  25413  nfprod  25414  indexa  26515  filbcmb  26535  sdclem2  26555  sdclem1  26556  fdc1  26559  rexrabdioph  26978  rexfrabdioph  26979  elnn0rabdioph  26987  dvdsrabdioph  26994  infrglb  27825  climinff  27840  stoweidlem53  27905  stoweidlem57  27909  cbvrex2  28054  bnj873  29272  bnj1014  29308  bnj1123  29332  bnj1307  29369  bnj1445  29390  bnj1446  29391  bnj1467  29400  bnj1463  29401
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-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator