Theorem nfralw 3285

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3337 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 1-Sep-1999.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 13-Dec-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		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	nfcrii 2894	. . 3 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
3		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
4	3	nf5ri 2203	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
5	2, 4	hbral 3282	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑)
6	5	nf5i 2152	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  Ⅎwnf 1785  Ⅎwnfc 2884  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053

This theorem is referenced by:  rspc2  3574  sbcralt  3811  reu8nf  3816  rspc2vd  3886  raaan  4459  raaan2  4463  reusngf  4619  rexreusng  4624  reuprg0  4647  nfint  4900  nfiin  4967  disjxun  5084  nfpo  5538  nfso  5539  nffr  5597  nfse  5598  ralxpf  5795  reuop  6251  frpoinsg  6301  dff13f  7203  nfiso  7270  mpoeq123  7432  nfofr  7631  tfisg  7798  fiun  7889  f1iun  7890  fmpox  8013  ovmptss  8036  frpoins3xpg  8083  nffrecs  8226  xpf1o  9070  ac6sfi  9187  nfoi  9422  setinds  9661  frinsg  9666  scottexs  9802  scott0s  9803  lble  12099  nnwof  12855  fzrevral  13557  reuccatpfxs1  14700  rlimcld2  15531  fsum2dlem  15723  fsumcom2  15727  fprod2dlem  15936  fprodcom2  15940  gsummoncoe1  22283  cnmpt21  23646  cfilucfil  24534  ulmss  26375  fsumdvdscom  27162  dchrisumlema  27465  dchrisumlem2  27467  nosupbnd1  27692  noinfbnd1  27707  cnlnadjlem5  32157  rspc2daf  32550  disjabrex  32667  disjabrexf  32668  aciunf1lem  32750  fnpreimac  32758  fsumiunle  32917  nsgqusf1olem1  33488  ordtconnlem1  34084  esumiun  34254  bnj1366  34987  bnj1385  34990  bnj981  35108  bnj1228  35169  bnj1398  35192  bnj1445  35202  bnj1449  35206  bnj1463  35213  untsucf  35908  poimirlem26  37981  poimirlem27  37982  indexdom  38069  filbcmb  38075  sdclem1  38078  scottexf  38503  scott0f  38504  cdleme31sn1  40841  cdlemk36  41373  setindtrs  43471  oaun3lem1  43820  nfscott  44684  scottabf  44685  nfrelp  45394  modelaxrep  45426  evth2f  45464  evthf  45476  uzwo4  45502  disjinfi  45640  choicefi  45647  rnmptbd2lem  45695  rnmptbdlem  45702  ssfiunibd  45760  infxrunb2  45815  supxrunb3  45846  supxrleubrnmpt  45852  allbutfiinf  45866  suprleubrnmpt  45868  infxrgelbrnmpt  45900  caucvgbf  45935  climinff  46059  limsupre3uzlem  46181  xlimmnfv  46280  xlimpnfv  46284  cncfshift  46320  cncficcgt0  46334  stoweidlem31  46477  stoweidlem34  46480  stoweidlem35  46481  stoweidlem51  46497  stoweidlem53  46499  stoweidlem54  46500  stoweidlem57  46503  stoweidlem59  46505  stoweidlem60  46506  fourierdlem31  46584  fourierdlem73  46625  iundjiun  46906  meaiuninc3v  46930  issmfle  47191  issmfgt  47202  issmfge  47216  smfpimcc  47254  smfsup  47260  smfinf  47264  2reu3  47570  2reu8i  47573  ichreuopeq  47945  reupr  47994  reuopreuprim  47998