Theorem nfralw 3309

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

This proof depends on syntax axioms:  Ⅎwnf 1816  Ⅎwnfc 2907  ∀wral 3076

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 2147  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2835  df-nfc 2909  df-ral 3077

This theorem is used by:  rspc2  3585  sbcralt  3819  reu8nf  3824  rspc2vd  3895  raaan  4474  raaan2  4478  reusngf  4635  rexreusng  4640  reuprg0  4663  nfint  4917  nfiin  4983  disjxun  5101  nfpo  5569  nfso  5570  nffr  5628  nfse  5629  ralxpf  5828  reuop  6293  frpoinsg  6343  dff13f  7255  nfiso  7326  mpoeq123  7488  nfofr  7691  tfisg  7856  fiun  7946  f1iun  7947  fmpox  8069  ovmptss  8095  frpoins3xpg  8143  nffrecs  8287  xpf1o  9144  ac6sfi  9261  nfoi  9493  setinds  9735  frinsg  9740  nfscott  9896  scottabf  9903  scottexsOLD  9907  scott0bsOLD  9909  lble  12216  nnwof  12988  fzrevral  13692  reuccatpfxs1  14841  rlimcld2  15690  fsum2dlem  15881  fsumcom2  15885  fprod2dlem  16092  fprodcom2  16096  gsummoncoe1  22565  cnmpt21  23929  cfilucfil  24817  ulmss  26665  fsumdvdscom  27453  dchrisumlema  27756  dchrisumlem2  27758  nosupbnd1  27982  noinfbnd1  27997  cnlnadjlem5  32584  rspc2daf  32974  disjabrex  33087  disjabrexf  33088  aciunf1lem  33167  fnpreimac  33175  fsumiunle  33331  nsgqusf1olem1  33875  ordtconnlem1  34467  esumiun  34637  bnj1366  35371  bnj1385  35374  bnj981  35492  bnj1228  35553  bnj1398  35576  bnj1445  35586  bnj1449  35590  bnj1463  35597  untsucf  36372  poimirlem26  38460  poimirlem27  38461  indexdom  38549  filbcmb  38555  sdclem1  38558  scottexf  38981  scott0f  38982  cdleme31sn1  41319  cdlemk36  41851  setindtrs  43931  oaun3lem1  44280  nfrelp  45837  modelaxrep  45869  evth2f  45914  evthf  45926  uzwo4  45952  disjinfi  46089  choicefi  46096  rnmptbd2lem  46142  rnmptbdlem  46149  ssfiunibd  46207  infxrunb2  46262  supxrunb3  46293  supxrleubrnmpt  46299  allbutfiinf  46313  suprleubrnmpt  46315  infxrgelbrnmpt  46347  caucvgbf  46382  climinff  46506  limsupre3uzlem  46628  xlimmnfv  46727  xlimpnfv  46731  cncfshift  46767  cncficcgt0  46781  stoweidlem31  46924  stoweidlem34  46927  stoweidlem35  46928  stoweidlem51  46944  stoweidlem53  46946  stoweidlem54  46947  stoweidlem57  46950  stoweidlem59  46952  stoweidlem60  46953  fourierdlem31  47031  fourierdlem73  47072  iundjiun  47353  meaiuninc3v  47377  issmfle  47638  issmfgt  47649  issmfge  47663  smfpimcc  47701  smfsup  47707  smfinf  47711  2reu3  48063  2reu8i  48066  ichreuopeq  48438  reupr  48487  reuopreuprim  48491  nfrals  50798  nfralseu  50829