Theorem nfralw 3312

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

This proof depends on syntax axioms:  Ⅎwnf 1813  Ⅎwnfc 2910  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-10 2176  ax-11 2192  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-clel 2838  df-nfc 2912  df-ral 3080

This theorem is used by:  rspc2  3590  sbcralt  3825  reu8nf  3830  rspc2vd  3901  raaan  4479  raaan2  4483  reusngf  4640  rexreusng  4645  reuprg0  4668  nfint  4922  nfiin  4989  disjxun  5107  nfpo  5575  nfso  5576  nffr  5634  nfse  5635  ralxpf  5832  reuop  6294  frpoinsg  6344  dff13f  7253  nfiso  7320  mpoeq123  7482  nfofr  7681  tfisg  7846  fiun  7936  f1iun  7937  fmpox  8060  ovmptss  8084  frpoins3xpg  8132  nffrecs  8276  xpf1o  9123  ac6sfi  9240  nfoi  9472  setinds  9714  frinsg  9719  nfscott  9857  scottabf  9864  scottexsOLD  9868  scott0bsOLD  9870  lble  12171  nnwof  12942  fzrevral  13645  reuccatpfxs1  14789  rlimcld2  15634  fsum2dlem  15826  fsumcom2  15830  fprod2dlem  16039  fprodcom2  16043  gsummoncoe1  22477  cnmpt21  23837  cfilucfil  24725  ulmss  26569  fsumdvdscom  27358  dchrisumlema  27661  dchrisumlem2  27663  nosupbnd1  27887  noinfbnd1  27902  cnlnadjlem5  32432  rspc2daf  32822  disjabrex  32936  disjabrexf  32937  aciunf1lem  33016  fnpreimac  33024  fsumiunle  33182  nsgqusf1olem1  33731  ordtconnlem1  34323  esumiun  34493  bnj1366  35226  bnj1385  35229  bnj981  35347  bnj1228  35408  bnj1398  35431  bnj1445  35441  bnj1449  35445  bnj1463  35452  untsucf  36210  poimirlem26  38325  poimirlem27  38326  indexdom  38413  filbcmb  38419  sdclem1  38422  scottexf  38845  scott0f  38846  cdleme31sn1  41183  cdlemk36  41715  setindtrs  43780  oaun3lem1  44129  nfrelp  45686  modelaxrep  45718  evth2f  45763  evthf  45775  uzwo4  45801  disjinfi  45938  choicefi  45945  rnmptbd2lem  45991  rnmptbdlem  45998  ssfiunibd  46056  infxrunb2  46111  supxrunb3  46142  supxrleubrnmpt  46148  allbutfiinf  46162  suprleubrnmpt  46164  infxrgelbrnmpt  46196  caucvgbf  46231  climinff  46355  limsupre3uzlem  46477  xlimmnfv  46576  xlimpnfv  46580  cncfshift  46616  cncficcgt0  46630  stoweidlem31  46773  stoweidlem34  46776  stoweidlem35  46777  stoweidlem51  46793  stoweidlem53  46795  stoweidlem54  46796  stoweidlem57  46799  stoweidlem59  46801  stoweidlem60  46802  fourierdlem31  46880  fourierdlem73  46921  iundjiun  47202  meaiuninc3v  47226  issmfle  47487  issmfgt  47498  issmfge  47512  smfpimcc  47550  smfsup  47556  smfinf  47560  2reu3  47875  2reu8i  47878  ichreuopeq  48250  reupr  48299  reuopreuprim  48303  nfrals  50610  nfralseu  50641