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

Theorem nfral 2974
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 𝑥𝐴
nfral.2 𝑥𝜑
Assertion
Ref Expression
nfral 𝑥𝑦𝐴 𝜑

Proof of Theorem nfral
StepHypRef Expression
1 nftru 1770 . . 3 𝑦
2 nfral.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfral.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrald 2973 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76trud 1533 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1524  wnf 1748  wnfc 2780  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946
This theorem is referenced by:  nfra2  2975  rspc2  3351  sbcralt  3543  reu8nf  3549  raaan  4115  nfint  4518  nfiin  4581  disjxun  4683  nfpo  5069  nfso  5070  nffr  5117  nfse  5118  ralxpf  5301  wfisg  5753  dff13f  6553  nfiso  6612  mpt2eq123  6756  fun11iun  7168  fmpt2x  7281  ovmptss  7303  nfwrecs  7454  xpf1o  8163  ac6sfi  8245  nfoi  8460  scottexs  8788  scott0s  8789  lble  11013  nnwof  11792  fzrevral  12463  reuccats1  13526  rlimcld2  14353  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  gsummoncoe1  19722  cnmpt21  21522  cfilucfil  22411  ulmss  24196  fsumdvdscom  24956  dchrisumlema  25222  dchrisumlem2  25224  rspc2vd  27245  cnlnadjlem5  29058  disjabrex  29521  disjabrexf  29522  aciunf1lem  29590  fsumiunle  29703  ordtconnlem1  30098  esumiun  30284  bnj1366  31026  bnj1385  31029  bnj981  31146  bnj1228  31205  bnj1398  31228  bnj1445  31238  bnj1449  31242  bnj1463  31249  untsucf  31713  setinds  31807  tfisg  31840  frpoinsg  31866  frinsg  31870  nffrecs  31903  nosupbnd1  31985  poimirlem26  33565  poimirlem27  33566  indexdom  33659  filbcmb  33665  sdclem1  33669  scottexf  34106  scott0f  34107  cdleme31sn1  35986  cdlemk36  36518  setindtrs  37909  evth2f  39488  evthf  39500  uzwo4  39535  eliuniincex  39606  disjinfi  39694  choicefi  39706  rnmptbd2lem  39777  rnmptbdlem  39784  ssfiunibd  39837  infxrunb2  39897  supxrunb3  39936  supxrleubrnmpt  39945  allbutfiinf  39960  suprleubrnmpt  39962  infxrgelbrnmpt  39996  climinff  40161  limsupre3uzlem  40285  xlimmnfv  40378  xlimpnfv  40382  cncfshift  40405  cncficcgt0  40419  stoweidlem31  40566  stoweidlem34  40569  stoweidlem35  40570  stoweidlem51  40586  stoweidlem53  40588  stoweidlem54  40589  stoweidlem57  40592  stoweidlem59  40594  stoweidlem60  40595  fourierdlem31  40673  fourierdlem73  40714  iundjiun  40995  meaiuninc3v  41019  issmfle  41275  issmfgt  41286  issmfge  41299  smfpimcc  41335  smfsup  41341  smfinf  41345  cbvral2  41493  raaan2  41496  2reu3  41509
  Copyright terms: Public domain W3C validator