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

Theorem nfral 3092
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 1899 . . 3 𝑦
2 nfral.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfral.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrald 3091 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76mptru 1660 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1653  wnf 1878  wnfc 2894  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060
This theorem is referenced by:  nfra2  3093  rspc2  3472  sbcralt  3669  reu8nf  3674  raaan  4239  nfint  4643  nfiin  4705  disjxun  4807  nfpo  5203  nfso  5204  nffr  5251  nfse  5252  ralxpf  5437  wfisg  5900  dff13f  6705  nfiso  6764  mpt2eq123  6912  nfofr  7101  fun11iun  7324  fmpt2x  7437  ovmptss  7460  nfwrecs  7612  xpf1o  8329  ac6sfi  8411  nfoi  8626  scottexs  8965  scott0s  8966  lble  11229  nnwof  11955  fzrevral  12632  reuccats1OLD  13726  reuccatpfxs1  13761  rlimcld2  14594  fsum2dlem  14786  fsumcom2  14790  fprod2dlem  14993  fprodcom2  14997  gsummoncoe1  19947  cnmpt21  21754  cfilucfil  22643  ulmss  24442  fsumdvdscom  25202  dchrisumlema  25468  dchrisumlem2  25470  rspc2vd  27545  cnlnadjlem5  29386  disjabrex  29843  disjabrexf  29844  aciunf1lem  29912  fsumiunle  30024  ordtconnlem1  30417  esumiun  30603  bnj1366  31348  bnj1385  31351  bnj981  31468  bnj1228  31527  bnj1398  31550  bnj1445  31560  bnj1449  31564  bnj1463  31571  untsucf  32033  setinds  32126  tfisg  32159  frpoinsg  32185  frinsg  32189  nffrecs  32222  nosupbnd1  32304  poimirlem26  33859  poimirlem27  33860  indexdom  33952  filbcmb  33958  sdclem1  33961  scottexf  34397  scott0f  34398  cdleme31sn1  36337  cdlemk36  36869  setindtrs  38269  evth2f  39826  evthf  39838  uzwo4  39872  eliuniincex  39942  disjinfi  40027  choicefi  40037  rnmptbd2lem  40104  rnmptbdlem  40111  ssfiunibd  40162  infxrunb2  40222  supxrunb3  40260  supxrleubrnmpt  40269  allbutfiinf  40284  suprleubrnmpt  40286  infxrgelbrnmpt  40320  climinff  40481  limsupre3uzlem  40605  xlimmnfv  40698  xlimpnfv  40702  cncfshift  40725  cncficcgt0  40739  stoweidlem31  40885  stoweidlem34  40888  stoweidlem35  40889  stoweidlem51  40905  stoweidlem53  40907  stoweidlem54  40908  stoweidlem57  40911  stoweidlem59  40913  stoweidlem60  40914  fourierdlem31  40992  fourierdlem73  41033  iundjiun  41314  meaiuninc3v  41338  issmfle  41594  issmfgt  41605  issmfge  41618  smfpimcc  41654  smfsup  41660  smfinf  41664  raaan2  41807  cbvral2  41844  2reu3  41859
  Copyright terms: Public domain W3C validator