Theorem nfralw 3149

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3150 with a disjoint variable condition, which does not require ax-13 2372. (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

Step	Hyp	Ref	Expression
1		nftru 1808	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfraldw 3146	. 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1546	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1787  Ⅎwnfc 2886  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-10 2139  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-clel 2817  df-nfc 2888  df-ral 3068

This theorem is referenced by:  nfra2wOLDOLD  3153  rspc2  3560  sbcralt  3801  reu8nf  3806  rspc2vd  3879  raaan  4448  raaan2  4452  reusngf  4605  rexreusng  4612  reuprg0  4635  nfint  4886  nfiin  4952  disjxun  5068  nfpo  5499  nfso  5500  nffr  5554  nfse  5555  ralxpf  5744  reuop  6185  frpoinsg  6231  wfisgOLD  6242  dff13f  7110  nfiso  7173  mpoeq123  7325  nfofr  7518  fiun  7759  f1iun  7760  fmpox  7880  ovmptss  7904  nffrecs  8070  nfwrecsOLD  8104  xpf1o  8875  ac6sfi  8988  nfoi  9203  frinsg  9440  scottexs  9576  scott0s  9577  lble  11857  nnwof  12583  fzrevral  13270  reuccatpfxs1  14388  rlimcld2  15215  fsum2dlem  15410  fsumcom2  15414  fprod2dlem  15618  fprodcom2  15622  gsummoncoe1  21385  cnmpt21  22730  cfilucfil  23621  ulmss  25461  fsumdvdscom  26239  dchrisumlema  26541  dchrisumlem2  26543  cnlnadjlem5  30334  rspc2daf  30717  disjabrex  30822  disjabrexf  30823  aciunf1lem  30901  fnpreimac  30910  fsumiunle  31045  nsgqusf1olem1  31500  ordtconnlem1  31776  esumiun  31962  bnj1366  32709  bnj1385  32712  bnj981  32830  bnj1228  32891  bnj1398  32914  bnj1445  32924  bnj1449  32928  bnj1463  32935  untsucf  33551  setinds  33660  tfisg  33692  frpoins3xpg  33714  nosupbnd1  33844  noinfbnd1  33859  poimirlem26  35730  poimirlem27  35731  indexdom  35819  filbcmb  35825  sdclem1  35828  scottexf  36253  scott0f  36254  cdleme31sn1  38322  cdlemk36  38854  setindtrs  40763  nfscott  41746  scottabf  41747  evth2f  42447  evthf  42459  uzwo4  42490  disjinfi  42620  choicefi  42629  rnmptbd2lem  42683  rnmptbdlem  42690  ssfiunibd  42738  infxrunb2  42797  supxrunb3  42829  supxrleubrnmpt  42836  allbutfiinf  42850  suprleubrnmpt  42852  infxrgelbrnmpt  42884  climinff  43042  limsupre3uzlem  43166  xlimmnfv  43265  xlimpnfv  43269  cncfshift  43305  cncficcgt0  43319  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem51  43482  stoweidlem53  43484  stoweidlem54  43485  stoweidlem57  43488  stoweidlem59  43490  stoweidlem60  43491  fourierdlem31  43569  fourierdlem73  43610  iundjiun  43888  meaiuninc3v  43912  issmfle  44168  issmfgt  44179  issmfge  44192  smfpimcc  44228  smfsup  44234  smfinf  44238  2reu3  44489  2reu8i  44492  ichreuopeq  44813  reupr  44862  reuopreuprim  44866