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

Theorem nfral 2719
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 1560 . . 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 2717 . 2  |-  (  T. 
->  F/ x A. y  e.  A  ph )
76trud 1329 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:    T. wtru 1322   F/wnf 1550   F/_wnfc 2527   A.wral 2666
This theorem is referenced by:  nfra2  2720  nfrex  2721  rspc2  3017  sbcralt  3193  sbcralg  3195  raaan  3695  nfint  4020  nfiin  4080  disjxun  4170  nfpo  4468  nfso  4469  nffr  4516  nfse  4517  ralxpf  4978  fun11iun  5654  dff13f  5965  nfiso  6003  mpt2eq123  6092  fmpt2x  6376  ovmptss  6387  nfrecs  6594  xpf1o  7228  ac6sfi  7310  nfoi  7439  scottexs  7767  scott0s  7768  lble  9916  nnwof  10499  fzrevral  11086  rlimcld2  12327  fsum2dlem  12509  fsumcom2  12513  cnmpt21  17656  cfilucfilOLD  18552  cfilucfil  18553  ulmss  20266  fsumdvdscom  20923  dchrisumlema  21135  dchrisumlem2  21137  cnlnadjlem5  23527  disjabrex  23977  disjabrexf  23978  untsucf  25112  fprod2dlem  25257  fprodcom2  25261  setinds  25348  tfisg  25418  wfisg  25423  frinsg  25459  indexdom  26326  filbcmb  26332  sdclem1  26337  setindtrs  26986  evth2f  27553  evthf  27565  climinff  27604  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem51  27667  stoweidlem53  27669  stoweidlem54  27670  stoweidlem57  27673  stoweidlem59  27675  stoweidlem60  27676  cbvral2  27817  raaan2  27820  2reu3  27833  bnj1366  28907  bnj1385  28910  bnj981  29027  bnj1228  29086  bnj1398  29109  bnj1445  29119  bnj1449  29123  bnj1463  29130  cdleme31sn1  30863  cdlemk36  31395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671
  Copyright terms: Public domain W3C validator