Theorem nfralw 3308

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

Syntax hints:  Ⅎwnf 1779   ∈ wcel 2105  Ⅎwnfc 2887  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-10 2138  ax-11 2154  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-nf 1780  df-clel 2813  df-nfc 2889  df-ral 3059

This theorem is referenced by:  rspc2  3630  sbcralt  3880  reu8nf  3885  rspc2vd  3958  raaan  4522  raaan2  4526  reusngf  4678  rexreusng  4683  reuprg0  4706  nfint  4960  nfiin  5028  disjxun  5145  nfpo  5602  nfso  5603  nffr  5661  nfse  5662  ralxpf  5859  reuop  6314  frpoinsg  6365  wfisgOLD  6376  dff13f  7275  nfiso  7341  mpoeq123  7504  nfofr  7703  tfisg  7874  fiun  7965  f1iun  7966  fmpox  8090  ovmptss  8116  frpoins3xpg  8163  nffrecs  8306  nfwrecsOLD  8340  xpf1o  9177  ac6sfi  9317  nfoi  9551  frinsg  9788  scottexs  9924  scott0s  9925  lble  12217  nnwof  12953  fzrevral  13648  reuccatpfxs1  14781  rlimcld2  15610  fsum2dlem  15802  fsumcom2  15806  fprod2dlem  16012  fprodcom2  16016  gsummoncoe1  22327  cnmpt21  23694  cfilucfil  24587  ulmss  26454  fsumdvdscom  27242  dchrisumlema  27546  dchrisumlem2  27548  nosupbnd1  27773  noinfbnd1  27788  cnlnadjlem5  32099  rspc2daf  32494  disjabrex  32601  disjabrexf  32602  aciunf1lem  32678  fnpreimac  32687  fsumiunle  32835  nsgqusf1olem1  33420  ordtconnlem1  33884  esumiun  34074  bnj1366  34821  bnj1385  34824  bnj981  34942  bnj1228  35003  bnj1398  35026  bnj1445  35036  bnj1449  35040  bnj1463  35047  untsucf  35689  setinds  35759  poimirlem26  37632  poimirlem27  37633  indexdom  37720  filbcmb  37726  sdclem1  37729  scottexf  38154  scott0f  38155  cdleme31sn1  40363  cdlemk36  40895  setindtrs  43013  oaun3lem1  43363  nfscott  44234  scottabf  44235  modelaxrep  44945  evth2f  44952  evthf  44964  uzwo4  44992  disjinfi  45134  choicefi  45142  rnmptbd2lem  45192  rnmptbdlem  45199  ssfiunibd  45259  infxrunb2  45317  supxrunb3  45348  supxrleubrnmpt  45355  allbutfiinf  45369  suprleubrnmpt  45371  infxrgelbrnmpt  45403  caucvgbf  45439  climinff  45566  limsupre3uzlem  45690  xlimmnfv  45789  xlimpnfv  45793  cncfshift  45829  cncficcgt0  45843  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem51  46006  stoweidlem53  46008  stoweidlem54  46009  stoweidlem57  46012  stoweidlem59  46014  stoweidlem60  46015  fourierdlem31  46093  fourierdlem73  46134  iundjiun  46415  meaiuninc3v  46439  issmfle  46700  issmfgt  46711  issmfge  46725  smfpimcc  46763  smfsup  46769  smfinf  46773  2reu3  47059  2reu8i  47062  ichreuopeq  47397  reupr  47446  reuopreuprim  47450