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

Theorem nfral 2785
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 1687 . . 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 2784 . 2  |-  ( T. 
->  F/ x A. y  e.  A  ph )
76trud 1463 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1455   F/wnf 1677   F/_wnfc 2589   A.wral 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753
This theorem is referenced by:  nfra2  2786  nfrexOLD  2862  rspc2  3169  sbcralt  3351  raaan  3888  nfint  4257  nfiin  4320  disjxun  4413  nfpo  4778  nfso  4779  nffr  4826  nfse  4827  ralxpf  4999  wfisg  5433  dff13f  6184  nfiso  6239  mpt2eq123  6376  fun11iun  6779  fmpt2x  6885  ovmptss  6903  nfwrecs  7055  xpf1o  7759  ac6sfi  7840  nfoi  8054  scottexs  8383  scott0s  8384  lble  10585  nnwof  11253  fzrevral  11907  rlimcld2  13690  fsum2dlem  13879  fsumcom2  13883  fprod2dlem  14082  fprodcom2  14086  gsummoncoe1  18946  cnmpt21  20734  cfilucfil  21622  ulmss  23400  fsumdvdscom  24162  dchrisumlema  24374  dchrisumlem2  24376  cnlnadjlem5  27772  disjabrex  28240  disjabrexf  28241  aciunf1lem  28312  ordtconlem1  28778  esumiun  28963  bnj1366  29689  bnj1385  29692  bnj981  29809  bnj1228  29868  bnj1398  29891  bnj1445  29901  bnj1449  29905  bnj1463  29912  untsucf  30385  setinds  30472  tfisg  30505  frinsg  30531  poimirlem26  32010  poimirlem27  32011  indexdom  32105  filbcmb  32111  sdclem1  32116  scottexf  32455  scott0f  32456  cdleme31sn1  33992  cdlemk36  34524  setindtrs  35924  evth2f  37375  evthf  37387  uzwo4  37429  disjinfi  37505  choicefi  37518  ssfiunibd  37564  climinff  37727  climinffOLD  37728  cncfshift  37788  cncficcgt0  37803  stoweidlem31  37929  stoweidlem34  37932  stoweidlem35  37933  stoweidlem51  37949  stoweidlem53  37951  stoweidlem54  37952  stoweidlem57  37955  stoweidlem59  37957  stoweidlem60  37958  fourierdlem31  38037  fourierdlem31OLD  38038  fourierdlem73  38080  iundjiun  38335  cbvral2  38630  raaan2  38633  2reu3  38646
  Copyright terms: Public domain W3C validator