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

Theorem nfrex 2766
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 2723 . 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 1835 . . . 4  |-  F/ x  -.  ph
52, 4nfral 2764 . . 3  |-  F/ x A. y  e.  A  -.  ph
65nfn 1835 . 2  |-  F/ x  -.  A. y  e.  A  -.  ph
71, 6nfxfr 1615 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   F/wnf 1589   F/_wnfc 2561   A.wral 2710   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716
This theorem is referenced by:  r19.12  2825  sbcrexgOLD  3267  nfuni  4092  nfiun  4193  nffr  4689  abrexex2g  6549  abrexex2  6553  nfrecs  6826  indexfi  7611  nfoi  7720  ixpiunwdom  7798  hsmexlem2  8588  iunfo  8695  iundom2g  8696  reclem2pr  9209  nfwrd  12248  nfsum1  13159  nfsum  13160  ptclsg  19163  iunmbl2  21013  mbfsup  21117  limciun  21344  iundisjf  25882  xrofsup  26006  nfcprod1  27374  nfcprod  27375  indexa  28580  filbcmb  28587  sdclem2  28591  sdclem1  28592  fdc1  28595  rexrabdioph  29085  rexfrabdioph  29086  elnn0rabdioph  29094  dvdsrabdioph  29101  infrglb  29724  climinff  29737  stoweidlem53  29801  stoweidlem57  29805  cbvrex2  29950  rabasiun  30183  bnj873  31804  bnj1014  31840  bnj1123  31864  bnj1307  31901  bnj1445  31922  bnj1446  31923  bnj1467  31932  bnj1463  31933
  Copyright terms: Public domain W3C validator