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

Theorem nfrex 2883
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 2850 . 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 1837 . . . 4  |-  F/ x  -.  ph
52, 4nfral 2881 . . 3  |-  F/ x A. y  e.  A  -.  ph
65nfn 1837 . 2  |-  F/ x  -.  A. y  e.  A  -.  ph
71, 6nfxfr 1616 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   F/wnf 1590   F/_wnfc 2599   A.wral 2795   E.wrex 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801
This theorem is referenced by:  r19.12  2929  sbcrexgOLD  3373  nfuni  4198  nfiun  4299  nffr  4795  abrexex2g  6657  abrexex2  6661  nfrecs  6937  indexfi  7723  nfoi  7832  ixpiunwdom  7910  hsmexlem2  8700  iunfo  8807  iundom2g  8808  reclem2pr  9321  nfwrd  12367  nfsum1  13278  nfsum  13279  ptclsg  19313  iunmbl2  21164  mbfsup  21268  limciun  21495  iundisjf  26075  xrofsup  26199  nfcprod1  27560  nfcprod  27561  indexa  28768  filbcmb  28775  sdclem2  28779  sdclem1  28780  fdc1  28783  rexrabdioph  29273  rexfrabdioph  29274  elnn0rabdioph  29282  dvdsrabdioph  29289  infrglb  29912  climinff  29925  stoweidlem53  29989  stoweidlem57  29993  cbvrex2  30138  rabasiun  30371  bnj873  32220  bnj1014  32256  bnj1123  32280  bnj1307  32317  bnj1445  32338  bnj1446  32339  bnj1467  32348  bnj1463  32349
  Copyright terms: Public domain W3C validator