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

Theorem nfral 2768
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 1634 . . 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 2767 . 2  |-  ( T. 
->  F/ x A. y  e.  A  ph )
76trud 1408 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1400   F/wnf 1624   F/_wnfc 2530   A.wral 2732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737
This theorem is referenced by:  nfra2  2769  nfrexOLD  2846  rspc2  3143  sbcralt  3325  raaan  3853  nfint  4209  nfiin  4272  disjxun  4365  nfpo  4719  nfso  4720  nffr  4767  nfse  4768  ralxpf  5062  dff13f  6068  nfiso  6121  mpt2eq123  6255  fun11iun  6659  fmpt2x  6765  ovmptss  6780  nfrecs  6962  xpf1o  7598  ac6sfi  7679  nfoi  7854  scottexs  8218  scott0s  8219  lble  10411  nnwof  11067  fzrevral  11685  rlimcld2  13403  fsum2dlem  13587  fsumcom2  13591  fprod2dlem  13786  fprodcom2  13790  gsummoncoe1  18459  cnmpt21  20257  cfilucfilOLD  21157  cfilucfil  21158  ulmss  22877  fsumdvdscom  23578  dchrisumlema  23790  dchrisumlem2  23792  cnlnadjlem5  27106  disjabrex  27572  disjabrexf  27573  aciunf1lem  27648  ordtconlem1  28060  esumiun  28242  untsucf  29248  setinds  29375  tfisg  29449  wfisg  29454  frinsg  29490  nfwrecs  29503  indexdom  30391  filbcmb  30397  sdclem1  30402  scottexf  30742  scott0f  30743  setindtrs  31133  evth2f  31557  evthf  31569  ssfiunibd  31675  climinff  31783  cncfshift  31842  cncficcgt0  31857  stoweidlem31  31979  stoweidlem34  31982  stoweidlem35  31983  stoweidlem51  31999  stoweidlem53  32001  stoweidlem54  32002  stoweidlem57  32005  stoweidlem59  32007  stoweidlem60  32008  fourierdlem31  32086  fourierdlem73  32128  cbvral2  32343  raaan2  32346  2reu3  32359  bnj1366  34235  bnj1385  34238  bnj981  34355  bnj1228  34414  bnj1398  34437  bnj1445  34447  bnj1449  34451  bnj1463  34458  cdleme31sn1  36520  cdlemk36  37052
  Copyright terms: Public domain W3C validator