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

Theorem nfral 2845
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 1604 . . 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 2844 . 2  |-  ( T. 
->  F/ x A. y  e.  A  ph )
76trud 1383 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1375   F/wnf 1594   F/_wnfc 2610   A.wral 2809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814
This theorem is referenced by:  nfra2  2846  nfrexOLD  2923  rspc2  3217  sbcralt  3407  raaan  3930  nfint  4287  nfiin  4349  disjxun  4440  nfpo  4800  nfso  4801  nffr  4848  nfse  4849  ralxpf  5142  dff13f  6148  nfiso  6201  mpt2eq123  6333  fun11iun  6736  fmpt2x  6842  ovmptss  6856  nfrecs  7036  xpf1o  7671  ac6sfi  7755  nfoi  7930  scottexs  8296  scott0s  8297  lble  10486  nnwof  11139  fzrevral  11753  rlimcld2  13352  fsum2dlem  13536  fsumcom2  13540  gsummoncoe1  18112  cnmpt21  19902  cfilucfilOLD  20802  cfilucfil  20803  ulmss  22521  fsumdvdscom  23184  dchrisumlema  23396  dchrisumlem2  23398  cnlnadjlem5  26654  disjabrex  27104  disjabrexf  27105  ordtconlem1  27530  untsucf  28545  fprod2dlem  28675  fprodcom2  28679  setinds  28775  tfisg  28849  wfisg  28854  frinsg  28890  nfwrecs  28903  indexdom  29817  filbcmb  29823  sdclem1  29828  scottexf  30169  scott0f  30170  setindtrs  30562  evth2f  30925  evthf  30937  ssfiunibd  31043  climinff  31110  cncfshift  31169  cncficcgt0  31184  stoweidlem31  31288  stoweidlem34  31291  stoweidlem35  31292  stoweidlem51  31308  stoweidlem53  31310  stoweidlem54  31311  stoweidlem57  31314  stoweidlem59  31316  stoweidlem60  31317  fourierdlem31  31395  fourierdlem73  31437  cbvral2  31601  raaan2  31604  2reu3  31617  bnj1366  32844  bnj1385  32847  bnj981  32964  bnj1228  33023  bnj1398  33046  bnj1445  33056  bnj1449  33060  bnj1463  33067  cdleme31sn1  35054  cdlemk36  35586
  Copyright terms: Public domain W3C validator