Theorem nfralw 3284

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3336 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by NM, 1-Sep-1999.) Avoid ax-13 2376. (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 2893	. . 3 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
3		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
4	3	nf5ri 2203	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
5	2, 4	hbral 3281	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑)
6	5	nf5i 2152	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  Ⅎwnf 1785  Ⅎwnfc 2883  ∀wral 3051

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 2811  df-nfc 2885  df-ral 3052

This theorem is referenced by:  rspc2  3573  sbcralt  3810  reu8nf  3815  rspc2vd  3885  raaan  4458  raaan2  4462  reusngf  4618  rexreusng  4623  reuprg0  4646  nfint  4899  nfiin  4966  disjxun  5083  nfpo  5545  nfso  5546  nffr  5604  nfse  5605  ralxpf  5801  reuop  6257  frpoinsg  6307  dff13f  7210  nfiso  7277  mpoeq123  7439  nfofr  7638  tfisg  7805  fiun  7896  f1iun  7897  fmpox  8020  ovmptss  8043  frpoins3xpg  8090  nffrecs  8233  xpf1o  9077  ac6sfi  9194  nfoi  9429  setinds  9670  frinsg  9675  scottexs  9811  scott0s  9812  lble  12108  nnwof  12864  fzrevral  13566  reuccatpfxs1  14709  rlimcld2  15540  fsum2dlem  15732  fsumcom2  15736  fprod2dlem  15945  fprodcom2  15949  gsummoncoe1  22273  cnmpt21  23636  cfilucfil  24524  ulmss  26362  fsumdvdscom  27148  dchrisumlema  27451  dchrisumlem2  27453  nosupbnd1  27678  noinfbnd1  27693  cnlnadjlem5  32142  rspc2daf  32535  disjabrex  32652  disjabrexf  32653  aciunf1lem  32735  fnpreimac  32743  fsumiunle  32902  nsgqusf1olem1  33473  ordtconnlem1  34068  esumiun  34238  bnj1366  34971  bnj1385  34974  bnj981  35092  bnj1228  35153  bnj1398  35176  bnj1445  35186  bnj1449  35190  bnj1463  35197  untsucf  35892  poimirlem26  37967  poimirlem27  37968  indexdom  38055  filbcmb  38061  sdclem1  38064  scottexf  38489  scott0f  38490  cdleme31sn1  40827  cdlemk36  41359  setindtrs  43453  oaun3lem1  43802  nfscott  44666  scottabf  44667  nfrelp  45376  modelaxrep  45408  evth2f  45446  evthf  45458  uzwo4  45484  disjinfi  45622  choicefi  45629  rnmptbd2lem  45677  rnmptbdlem  45684  ssfiunibd  45742  infxrunb2  45797  supxrunb3  45828  supxrleubrnmpt  45834  allbutfiinf  45848  suprleubrnmpt  45850  infxrgelbrnmpt  45882  caucvgbf  45917  climinff  46041  limsupre3uzlem  46163  xlimmnfv  46262  xlimpnfv  46266  cncfshift  46302  cncficcgt0  46316  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem51  46479  stoweidlem53  46481  stoweidlem54  46482  stoweidlem57  46485  stoweidlem59  46487  stoweidlem60  46488  fourierdlem31  46566  fourierdlem73  46607  iundjiun  46888  meaiuninc3v  46912  issmfle  47173  issmfgt  47184  issmfge  47198  smfpimcc  47236  smfsup  47242  smfinf  47246  2reu3  47558  2reu8i  47561  ichreuopeq  47933  reupr  47982  reuopreuprim  47986