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

Theorem nfrex 2704
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 2662 . 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 1801 . . . 4  |-  F/ x  -.  ph
52, 4nfral 2702 . . 3  |-  F/ x A. y  e.  A  -.  ph
65nfn 1801 . 2  |-  F/ x  -.  A. y  e.  A  -.  ph
71, 6nfxfr 1576 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1550   F/_wnfc 2510   A.wral 2649   E.wrex 2650
This theorem is referenced by:  r19.12  2762  sbcrexg  3179  nfuni  3963  nfiun  4061  nffr  4497  abrexex2g  5927  abrexex2  5940  nfrecs  6571  indexfi  7349  nfoi  7416  ixpiunwdom  7492  hsmexlem2  8240  iunfo  8347  iundom2g  8348  reclem2pr  8858  nfwrd  11667  nfsum1  12411  nfsum  12412  ptclsg  17568  iunmbl2  19318  mbfsup  19423  limciun  19648  iundisjf  23872  xrofsup  23962  nfcprod1  25015  nfcprod  25016  indexa  26126  filbcmb  26133  sdclem2  26137  sdclem1  26138  fdc1  26141  rexrabdioph  26545  rexfrabdioph  26546  elnn0rabdioph  26554  dvdsrabdioph  26561  infrglb  27390  climinff  27405  stoweidlem53  27470  stoweidlem57  27474  cbvrex2  27619  bnj873  28633  bnj1014  28669  bnj1123  28693  bnj1307  28730  bnj1445  28751  bnj1446  28752  bnj1467  28761  bnj1463  28762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655
  Copyright terms: Public domain W3C validator