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

Theorem nfral 2843
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
nfral.2
Assertion
Ref Expression
nfral

Proof of Theorem nfral
StepHypRef Expression
1 nftru 1626 . . 3
2 nfral.1 . . . 4
32a1i 11 . . 3
4 nfral.2 . . . 4
54a1i 11 . . 3
61, 3, 5nfrald 2842 . 2
76trud 1404 1
Colors of variables: wff setvar class
Syntax hints:   wtru 1396  F/wnf 1616  F/_wnfc 2605  A.wral 2807
This theorem is referenced by:  nfra2  2844  nfrexOLD  2921  rspc2  3218  sbcralt  3408  raaan  3937  nfint  4296  nfiin  4359  disjxun  4450  nfpo  4810  nfso  4811  nffr  4858  nfse  4859  ralxpf  5154  dff13f  6167  nfiso  6220  mpt2eq123  6356  fun11iun  6760  fmpt2x  6866  ovmptss  6881  nfrecs  7063  xpf1o  7699  ac6sfi  7784  nfoi  7960  scottexs  8326  scott0s  8327  lble  10520  nnwof  11177  fzrevral  11792  rlimcld2  13401  fsum2dlem  13585  fsumcom2  13589  fprod2dlem  13784  fprodcom2  13788  gsummoncoe1  18346  cnmpt21  20172  cfilucfilOLD  21072  cfilucfil  21073  ulmss  22792  fsumdvdscom  23461  dchrisumlema  23673  dchrisumlem2  23675  cnlnadjlem5  26990  disjabrex  27443  disjabrexf  27444  ordtconlem1  27906  untsucf  29082  setinds  29210  tfisg  29284  wfisg  29289  frinsg  29325  nfwrecs  29338  indexdom  30225  filbcmb  30231  sdclem1  30236  scottexf  30576  scott0f  30577  setindtrs  30967  evth2f  31390  evthf  31402  ssfiunibd  31509  climinff  31617  cncfshift  31676  cncficcgt0  31691  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem51  31833  stoweidlem53  31835  stoweidlem54  31836  stoweidlem57  31839  stoweidlem59  31841  stoweidlem60  31842  fourierdlem31  31920  fourierdlem73  31962  cbvral2  32177  raaan2  32180  2reu3  32193  bnj1366  33888  bnj1385  33891  bnj981  34008  bnj1228  34067  bnj1398  34090  bnj1445  34100  bnj1449  34104  bnj1463  34111  cdleme31sn1  36107  cdlemk36  36639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812
  Copyright terms: Public domain W3C validator