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 1563 . . 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 1332 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:    T. wtru 1325   F/wnf 1553   F/_wnfc 2559   A.wral 2705
This theorem is referenced by:  nfra2  2760  nfrex  2761  rspc2  3057  sbcralt  3233  sbcralg  3235  raaan  3735  nfint  4060  nfiin  4120  disjxun  4210  nfpo  4508  nfso  4509  nffr  4556  nfse  4557  ralxpf  5019  fun11iun  5695  dff13f  6006  nfiso  6044  mpt2eq123  6133  fmpt2x  6417  ovmptss  6428  nfrecs  6635  xpf1o  7269  ac6sfi  7351  nfoi  7483  scottexs  7811  scott0s  7812  lble  9960  nnwof  10543  fzrevral  11131  rlimcld2  12372  fsum2dlem  12554  fsumcom2  12558  cnmpt21  17703  cfilucfilOLD  18599  cfilucfil  18600  ulmss  20313  fsumdvdscom  20970  dchrisumlema  21182  dchrisumlem2  21184  cnlnadjlem5  23574  disjabrex  24024  disjabrexf  24025  untsucf  25159  fprod2dlem  25304  fprodcom2  25308  setinds  25405  tfisg  25479  wfisg  25484  frinsg  25520  nfwrecs  25533  indexdom  26436  filbcmb  26442  sdclem1  26447  setindtrs  27096  evth2f  27662  evthf  27674  climinff  27713  stoweidlem31  27756  stoweidlem34  27759  stoweidlem35  27760  stoweidlem51  27776  stoweidlem53  27778  stoweidlem54  27779  stoweidlem57  27782  stoweidlem59  27784  stoweidlem60  27785  cbvral2  27926  raaan2  27929  2reu3  27942  bnj1366  29201  bnj1385  29204  bnj981  29321  bnj1228  29380  bnj1398  29403  bnj1445  29413  bnj1449  29417  bnj1463  29424  cdleme31sn1  31178  cdlemk36  31710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710
  Copyright terms: Public domain W3C validator