Theorem nfralw 3314

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

This proof depends on syntax axioms:  Ⅎwnf 1816  Ⅎwnfc 2912  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-10 2179  ax-11 2195  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2840  df-nfc 2914  df-ral 3082

This theorem is used by:  rspc2  3592  sbcralt  3826  reu8nf  3831  rspc2vd  3902  raaan  4481  raaan2  4485  reusngf  4642  rexreusng  4647  reuprg0  4670  nfint  4924  nfiin  4991  disjxun  5109  nfpo  5577  nfso  5578  nffr  5636  nfse  5637  ralxpf  5834  reuop  6299  frpoinsg  6349  dff13f  7259  nfiso  7330  mpoeq123  7492  nfofr  7692  tfisg  7857  fiun  7947  f1iun  7948  fmpox  8071  ovmptss  8095  frpoins3xpg  8143  nffrecs  8287  xpf1o  9135  ac6sfi  9252  nfoi  9484  setinds  9726  frinsg  9731  nfscott  9869  scottabf  9876  scottexsOLD  9880  scott0bsOLD  9882  lble  12187  nnwof  12959  fzrevral  13662  reuccatpfxs1  14811  rlimcld2  15658  fsum2dlem  15849  fsumcom2  15853  fprod2dlem  16062  fprodcom2  16066  gsummoncoe1  22523  cnmpt21  23884  cfilucfil  24772  ulmss  26616  fsumdvdscom  27405  dchrisumlema  27708  dchrisumlem2  27710  nosupbnd1  27934  noinfbnd1  27949  cnlnadjlem5  32499  rspc2daf  32889  disjabrex  33003  disjabrexf  33004  aciunf1lem  33083  fnpreimac  33091  fsumiunle  33248  nsgqusf1olem1  33791  ordtconnlem1  34383  esumiun  34553  bnj1366  35287  bnj1385  35290  bnj981  35408  bnj1228  35469  bnj1398  35492  bnj1445  35502  bnj1449  35506  bnj1463  35513  untsucf  36244  poimirlem26  38359  poimirlem27  38360  indexdom  38448  filbcmb  38454  sdclem1  38457  scottexf  38880  scott0f  38881  cdleme31sn1  41218  cdlemk36  41750  setindtrs  43830  oaun3lem1  44179  nfrelp  45736  modelaxrep  45768  evth2f  45813  evthf  45825  uzwo4  45851  disjinfi  45988  choicefi  45995  rnmptbd2lem  46041  rnmptbdlem  46048  ssfiunibd  46106  infxrunb2  46161  supxrunb3  46192  supxrleubrnmpt  46198  allbutfiinf  46212  suprleubrnmpt  46214  infxrgelbrnmpt  46246  caucvgbf  46281  climinff  46405  limsupre3uzlem  46527  xlimmnfv  46626  xlimpnfv  46630  cncfshift  46666  cncficcgt0  46680  stoweidlem31  46823  stoweidlem34  46826  stoweidlem35  46827  stoweidlem51  46843  stoweidlem53  46845  stoweidlem54  46846  stoweidlem57  46849  stoweidlem59  46851  stoweidlem60  46852  fourierdlem31  46930  fourierdlem73  46971  iundjiun  47252  meaiuninc3v  47276  issmfle  47537  issmfgt  47548  issmfge  47562  smfpimcc  47600  smfsup  47606  smfinf  47610  2reu3  47925  2reu8i  47928  ichreuopeq  48300  reupr  48349  reuopreuprim  48353  nfrals  50659  nfralseu  50690