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

Theorem nfrex 2761
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 2718 . 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 1834 . . . 4  |-  F/ x  -.  ph
52, 4nfral 2759 . . 3  |-  F/ x A. y  e.  A  -.  ph
65nfn 1834 . 2  |-  F/ x  -.  A. y  e.  A  -.  ph
71, 6nfxfr 1618 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   F/wnf 1592   F/_wnfc 2556   A.wral 2705   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711
This theorem is referenced by:  r19.12  2820  sbcrexgOLD  3260  nfuni  4085  nfiun  4186  nffr  4681  abrexex2g  6543  abrexex2  6547  nfrecs  6820  indexfi  7607  nfoi  7716  ixpiunwdom  7794  hsmexlem2  8584  iunfo  8691  iundom2g  8692  reclem2pr  9204  nfwrd  12239  nfsum1  13150  nfsum  13151  ptclsg  19029  iunmbl2  20879  mbfsup  20983  limciun  21210  iundisjf  25754  xrofsup  25877  nfcprod1  27269  nfcprod  27270  indexa  28468  filbcmb  28475  sdclem2  28479  sdclem1  28480  fdc1  28483  rexrabdioph  28974  rexfrabdioph  28975  elnn0rabdioph  28983  dvdsrabdioph  28990  infrglb  29614  climinff  29627  stoweidlem53  29691  stoweidlem57  29695  cbvrex2  29840  rabasiun  30073  bnj873  31616  bnj1014  31652  bnj1123  31676  bnj1307  31713  bnj1445  31734  bnj1446  31735  bnj1467  31744  bnj1463  31745
  Copyright terms: Public domain W3C validator