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

Theorem nfrex 2754
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 2711 . 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 1811 . . . 4  |-  F/ x  -.  ph
52, 4nfral 2752 . . 3  |-  F/ x A. y  e.  A  -.  ph
65nfn 1811 . 2  |-  F/ x  -.  A. y  e.  A  -.  ph
71, 6nfxfr 1579 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1553   F/_wnfc 2559   A.wral 2698   E.wrex 2699
This theorem is referenced by:  r19.12  2812  sbcrexg  3229  nfuni  4014  nfiun  4112  nffr  4549  abrexex2g  5981  abrexex2  5994  nfrecs  6628  indexfi  7407  nfoi  7476  ixpiunwdom  7552  hsmexlem2  8300  iunfo  8407  iundom2g  8408  reclem2pr  8918  nfwrd  11733  nfsum1  12477  nfsum  12478  ptclsg  17640  iunmbl2  19444  mbfsup  19549  limciun  19774  iundisjf  24022  xrofsup  24119  nfcprod1  25229  nfcprod  25230  indexa  26427  filbcmb  26434  sdclem2  26438  sdclem1  26439  fdc1  26442  rexrabdioph  26846  rexfrabdioph  26847  elnn0rabdioph  26855  dvdsrabdioph  26862  infrglb  27690  climinff  27705  stoweidlem53  27770  stoweidlem57  27774  cbvrex2  27919  bnj873  29233  bnj1014  29269  bnj1123  29293  bnj1307  29330  bnj1445  29351  bnj1446  29352  bnj1467  29361  bnj1463  29362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2703  df-rex 2704
  Copyright terms: Public domain W3C validator