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

Theorem nfral 2609
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 1544 . . 3  |-  F/ y  T.
2 nfral.1 . . . 4  |-  F/_ x A
32a1i 10 . . 3  |-  (  T. 
->  F/_ x A )
4 nfral.2 . . . 4  |-  F/ x ph
54a1i 10 . . 3  |-  (  T. 
->  F/ x ph )
61, 3, 5nfrald 2607 . 2  |-  (  T. 
->  F/ x A. y  e.  A  ph )
76trud 1314 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/wnf 1534   F/_wnfc 2419   A.wral 2556
This theorem is referenced by:  nfra2  2610  nfrex  2611  rspc2  2902  sbcralt  3076  sbcralg  3078  raaan  3574  nfint  3888  nfiin  3948  disjxun  4037  nfpo  4335  nfso  4336  nffr  4383  nfse  4384  ralxpf  4846  fun11iun  5509  dff13f  5800  nfiso  5837  mpt2eq123  5923  nfofr  6100  fmpt2x  6206  ovmptss  6216  nfrecs  6406  xpf1o  7039  ac6sfi  7117  nfoi  7245  scottexs  7573  scott0s  7574  lble  9722  nnwof  10301  fzrevral  10882  rlimcld2  12068  fsum2dlem  12249  fsumcom2  12253  cnmpt21  17381  ulmss  19790  fsumdvdscom  20441  dchrisumlema  20653  dchrisumlem2  20655  cnlnadjlem5  22667  disjabrex  23374  disjabrexf  23375  untsucf  24071  dedekind  24097  dedekindle  24098  setinds  24205  tfisg  24275  wfisg  24280  frinsg  24316  imonclem  25916  cmpmon  25918  iepiclem  25926  indexdom  26516  filbcmb  26535  sdclem1  26556  setindtrs  27221  evth2f  27789  evthf  27801  climinff  27840  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem51  27903  stoweidlem53  27905  stoweidlem54  27906  stoweidlem57  27909  stoweidlem59  27911  stoweidlem60  27912  cbvral2  28053  raaan2  28056  2reu3  28069  bnj1366  29178  bnj1379  29179  bnj1385  29181  bnj981  29298  bnj1228  29357  bnj1398  29380  bnj1445  29390  bnj1449  29394  bnj1463  29401  cdleme31sn1  31192  cdlemk36  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator