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

Theorem nfral 2759
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 1602 . . 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 2757 . 2  |-  ( T. 
->  F/ x A. y  e.  A  ph )
76trud 1371 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1363   F/wnf 1592   F/_wnfc 2556   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710
This theorem is referenced by:  nfra2  2760  nfrex  2761  rspc2  3067  sbcralt  3255  raaan  3775  nfint  4126  nfiin  4187  disjxun  4278  nfpo  4633  nfso  4634  nffr  4681  nfse  4682  ralxpf  4973  dff13f  5960  nfiso  6002  mpt2eq123  6134  fun11iun  6526  fmpt2x  6629  ovmptss  6643  nfrecs  6820  xpf1o  7461  ac6sfi  7544  nfoi  7716  scottexs  8082  scott0s  8083  lble  10269  nnwof  10908  fzrevral  11527  rlimcld2  13039  fsum2dlem  13220  fsumcom2  13224  cnmpt21  19085  cfilucfilOLD  19985  cfilucfil  19986  ulmss  21746  fsumdvdscom  22409  dchrisumlema  22621  dchrisumlem2  22623  cnlnadjlem5  25297  disjabrex  25749  disjabrexf  25750  ordtconlem1  26207  untsucf  27207  fprod2dlem  27337  fprodcom2  27341  setinds  27437  tfisg  27511  wfisg  27516  frinsg  27552  nfwrecs  27565  indexdom  28469  filbcmb  28475  sdclem1  28480  scottexf  28822  scott0f  28823  setindtrs  29216  evth2f  29579  evthf  29591  climinff  29627  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem51  29689  stoweidlem53  29691  stoweidlem54  29692  stoweidlem57  29695  stoweidlem59  29697  stoweidlem60  29698  cbvral2  29839  raaan2  29842  2reu3  29855  bnj1366  31522  bnj1385  31525  bnj981  31642  bnj1228  31701  bnj1398  31724  bnj1445  31734  bnj1449  31738  bnj1463  31745  cdleme31sn1  33595  cdlemk36  34127
  Copyright terms: Public domain W3C validator