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

Theorem nfrex 2927
Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.)
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 nftru 1609 . . 3  |-  F/ y T.
2 nfrex.1 . . . 4  |-  F/_ x A
32a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
4 nfrex.2 . . . 4  |-  F/ x ph
54a1i 11 . . 3  |-  ( T. 
->  F/ x ph )
61, 3, 5nfrexd 2926 . 2  |-  ( T. 
->  F/ x E. y  e.  A  ph )
76trud 1388 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1380   F/wnf 1599   F/_wnfc 2615   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820
This theorem is referenced by:  r19.12  2988  sbcrexgOLD  3417  nfuni  4251  rabasiun  4329  nfiun  4353  nffr  4853  abrexex2g  6758  abrexex2  6762  nfrecs  7041  indexfi  7824  nfoi  7935  ixpiunwdom  8013  hsmexlem2  8803  iunfo  8910  iundom2g  8911  reclem2pr  9422  nfwrd  12531  nfsum1  13471  nfsum  13472  ptclsg  19851  iunmbl2  21702  mbfsup  21806  limciun  22033  iundisjf  27121  xrofsup  27250  nfcprod1  28619  nfcprod  28620  indexa  29827  filbcmb  29834  sdclem2  29838  sdclem1  29839  fdc1  29842  rexrabdioph  30331  rexfrabdioph  30332  elnn0rabdioph  30340  dvdsrabdioph  30347  infrglb  31140  climinff  31153  cncfshift  31212  stoweidlem53  31353  stoweidlem57  31357  fourierdlem48  31455  fourierdlem73  31480  cbvrex2  31645  bnj873  33061  bnj1014  33097  bnj1123  33121  bnj1307  33158  bnj1445  33179  bnj1446  33180  bnj1467  33189  bnj1463  33190
  Copyright terms: Public domain W3C validator