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

Theorem nfrex 2598
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 2556 . 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 1765 . . . 4  |-  F/ x  -.  ph
52, 4nfral 2596 . . 3  |-  F/ x A. y  e.  A  -.  ph
65nfn 1765 . 2  |-  F/ x  -.  A. y  e.  A  -.  ph
71, 6nfxfr 1557 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1531   F/_wnfc 2406   A.wral 2543   E.wrex 2544
This theorem is referenced by:  r19.12  2656  sbcrexg  3066  nfuni  3833  nfiun  3931  nffr  4367  abrexex2g  5768  abrexex2  5780  nfrecs  6390  indexfi  7163  nfoi  7229  ixpiunwdom  7305  hsmexlem2  8053  iunfo  8161  iundom2g  8162  reclem2pr  8672  nfwrd  11426  nfsum1  12163  nfsum  12164  ptclsg  17309  iunmbl2  18914  mbfsup  19019  limciun  19244  xrofsup  23255  iundisjf  23365  nfprod1  25310  nfprod  25311  indexa  26412  filbcmb  26432  sdclem2  26452  sdclem1  26453  fdc1  26456  rexrabdioph  26875  rexfrabdioph  26876  elnn0rabdioph  26884  dvdsrabdioph  26891  infrglb  27722  climinff  27737  stoweidlem53  27802  stoweidlem57  27806  cbvrex2  27951  bnj873  28956  bnj1014  28992  bnj1123  29016  bnj1307  29053  bnj1445  29074  bnj1446  29075  bnj1467  29084  bnj1463  29085
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-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator