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

Theorem nfral 2829
Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfral.1  |-  F/_ x A
nfral.2  |-  F/ x ph
Assertion
Ref Expression
nfral  |-  F/ x A. y  e.  A  ph

Proof of Theorem nfral
StepHypRef Expression
1 nftru 1613 . . 3  |-  F/ y T.
2 nfral.1 . . . 4  |-  F/_ x A
32a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
4 nfral.2 . . . 4  |-  F/ x ph
54a1i 11 . . 3  |-  ( T. 
->  F/ x ph )
61, 3, 5nfrald 2828 . 2  |-  ( T. 
->  F/ x A. y  e.  A  ph )
76trud 1392 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1384   F/wnf 1603   F/_wnfc 2591   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798
This theorem is referenced by:  nfra2  2830  nfrexOLD  2907  rspc2  3204  sbcralt  3394  raaan  3922  nfint  4281  nfiin  4344  disjxun  4435  nfpo  4795  nfso  4796  nffr  4843  nfse  4844  ralxpf  5139  dff13f  6152  nfiso  6205  mpt2eq123  6341  fun11iun  6745  fmpt2x  6851  ovmptss  6866  nfrecs  7046  xpf1o  7681  ac6sfi  7766  nfoi  7942  scottexs  8308  scott0s  8309  lble  10502  nnwof  11159  fzrevral  11774  rlimcld2  13383  fsum2dlem  13567  fsumcom2  13571  fprod2dlem  13766  fprodcom2  13770  gsummoncoe1  18325  cnmpt21  20150  cfilucfilOLD  21050  cfilucfil  21051  ulmss  22770  fsumdvdscom  23439  dchrisumlema  23651  dchrisumlem2  23653  cnlnadjlem5  26968  disjabrex  27421  disjabrexf  27422  ordtconlem1  27884  untsucf  29060  setinds  29186  tfisg  29260  wfisg  29265  frinsg  29301  nfwrecs  29314  indexdom  30201  filbcmb  30207  sdclem1  30212  scottexf  30552  scott0f  30553  setindtrs  30943  evth2f  31344  evthf  31356  ssfiunibd  31463  climinff  31571  cncfshift  31630  cncficcgt0  31645  stoweidlem31  31767  stoweidlem34  31770  stoweidlem35  31771  stoweidlem51  31787  stoweidlem53  31789  stoweidlem54  31790  stoweidlem57  31793  stoweidlem59  31795  stoweidlem60  31796  fourierdlem31  31874  fourierdlem73  31916  cbvral2  32131  raaan2  32134  2reu3  32147  bnj1366  33756  bnj1385  33759  bnj981  33876  bnj1228  33935  bnj1398  33958  bnj1445  33968  bnj1449  33972  bnj1463  33979  cdleme31sn1  35982  cdlemk36  36514
  Copyright terms: Public domain W3C validator