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

Theorem nfralw 3228
Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3229 with a disjoint variable condition, which does not require ax-13 2389. (Contributed by NM, 1-Sep-1999.) (Revised by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
nfralw.1 𝑥𝐴
nfralw.2 𝑥𝜑
Assertion
Ref Expression
nfralw 𝑥𝑦𝐴 𝜑
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfralw
StepHypRef Expression
1 nftru 1804 . . 3 𝑦
2 nfralw.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfralw.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfraldw 3226 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76mptru 1543 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1537  wnf 1783  wnfc 2964  wral 3141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146
This theorem is referenced by:  nfra2w  3230  rspc2  3634  sbcralt  3858  reu8nf  3863  rspc2vd  3935  raaan  4463  raaan2  4467  reusngf  4615  rexreusng  4620  reuprg0  4641  nfint  4889  nfiin  4953  disjxun  5067  nfpo  5482  nfso  5483  nffr  5532  nfse  5533  ralxpf  5720  reuop  6147  wfisg  6186  dff13f  7017  nfiso  7078  mpoeq123  7229  nfofr  7418  fiun  7647  f1iun  7648  fmpox  7768  ovmptss  7791  nfwrecs  7952  xpf1o  8682  ac6sfi  8765  nfoi  8981  scottexs  9319  scott0s  9320  lble  11596  nnwof  12317  fzrevral  12995  reuccatpfxs1  14112  rlimcld2  14938  fsum2dlem  15128  fsumcom2  15132  fprod2dlem  15337  fprodcom2  15341  gsummoncoe1  20475  cnmpt21  22282  cfilucfil  23172  ulmss  24988  fsumdvdscom  25765  dchrisumlema  26067  dchrisumlem2  26069  cnlnadjlem5  29851  rspc2daf  30234  disjabrex  30335  disjabrexf  30336  aciunf1lem  30410  fnpreimac  30419  fsumiunle  30549  ordtconnlem1  31171  esumiun  31357  bnj1366  32105  bnj1385  32108  bnj981  32226  bnj1228  32287  bnj1398  32310  bnj1445  32320  bnj1449  32324  bnj1463  32331  untsucf  32940  setinds  33027  tfisg  33059  frpoinsg  33085  frinsg  33091  nffrecs  33124  nosupbnd1  33218  poimirlem26  34922  poimirlem27  34923  indexdom  35013  filbcmb  35019  sdclem1  35022  scottexf  35450  scott0f  35451  cdleme31sn1  37521  cdlemk36  38053  setindtrs  39628  nfscott  40581  scottabf  40582  evth2f  41278  evthf  41290  uzwo4  41321  disjinfi  41460  choicefi  41469  rnmptbd2lem  41526  rnmptbdlem  41533  ssfiunibd  41582  infxrunb2  41642  supxrunb3  41678  supxrleubrnmpt  41685  allbutfiinf  41700  suprleubrnmpt  41702  infxrgelbrnmpt  41736  climinff  41898  limsupre3uzlem  42022  xlimmnfv  42121  xlimpnfv  42125  cncfshift  42163  cncficcgt0  42177  stoweidlem31  42323  stoweidlem34  42326  stoweidlem35  42327  stoweidlem51  42343  stoweidlem53  42345  stoweidlem54  42346  stoweidlem57  42349  stoweidlem59  42351  stoweidlem60  42352  fourierdlem31  42430  fourierdlem73  42471  iundjiun  42749  meaiuninc3v  42773  issmfle  43029  issmfgt  43040  issmfge  43053  smfpimcc  43089  smfsup  43095  smfinf  43099  2reu3  43316  2reu8i  43319  ichreuopeq  43642  reupr  43691  reuopreuprim  43695
  Copyright terms: Public domain W3C validator