Theorem nfralw 3276

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045

This theorem is referenced by:  rspc2  3586  sbcralt  3824  reu8nf  3829  rspc2vd  3899  raaan  4468  raaan2  4472  reusngf  4626  rexreusng  4631  reuprg0  4654  nfint  4906  nfiin  4974  disjxun  5090  nfpo  5533  nfso  5534  nffr  5592  nfse  5593  ralxpf  5789  reuop  6241  frpoinsg  6291  dff13f  7192  nfiso  7259  mpoeq123  7421  nfofr  7620  tfisg  7787  fiun  7878  f1iun  7879  fmpox  8002  ovmptss  8026  frpoins3xpg  8073  nffrecs  8216  xpf1o  9056  ac6sfi  9173  nfoi  9406  frinsg  9647  scottexs  9783  scott0s  9784  lble  12077  nnwof  12815  fzrevral  13515  reuccatpfxs1  14653  rlimcld2  15485  fsum2dlem  15677  fsumcom2  15681  fprod2dlem  15887  fprodcom2  15891  gsummoncoe1  22193  cnmpt21  23556  cfilucfil  24445  ulmss  26304  fsumdvdscom  27093  dchrisumlema  27397  dchrisumlem2  27399  nosupbnd1  27624  noinfbnd1  27639  cnlnadjlem5  32015  rspc2daf  32410  disjabrex  32526  disjabrexf  32527  aciunf1lem  32606  fnpreimac  32615  fsumiunle  32775  nsgqusf1olem1  33351  ordtconnlem1  33897  esumiun  34067  bnj1366  34802  bnj1385  34805  bnj981  34923  bnj1228  34984  bnj1398  35007  bnj1445  35017  bnj1449  35021  bnj1463  35028  untsucf  35693  setinds  35762  poimirlem26  37636  poimirlem27  37637  indexdom  37724  filbcmb  37730  sdclem1  37733  scottexf  38158  scott0f  38159  cdleme31sn1  40370  cdlemk36  40902  setindtrs  43008  oaun3lem1  43357  nfscott  44222  scottabf  44223  nfrelp  44933  modelaxrep  44965  evth2f  45003  evthf  45015  uzwo4  45041  disjinfi  45180  choicefi  45188  rnmptbd2lem  45236  rnmptbdlem  45243  ssfiunibd  45301  infxrunb2  45357  supxrunb3  45388  supxrleubrnmpt  45395  allbutfiinf  45409  suprleubrnmpt  45411  infxrgelbrnmpt  45443  caucvgbf  45478  climinff  45602  limsupre3uzlem  45726  xlimmnfv  45825  xlimpnfv  45829  cncfshift  45865  cncficcgt0  45879  stoweidlem31  46022  stoweidlem34  46025  stoweidlem35  46026  stoweidlem51  46042  stoweidlem53  46044  stoweidlem54  46045  stoweidlem57  46048  stoweidlem59  46050  stoweidlem60  46051  fourierdlem31  46129  fourierdlem73  46170  iundjiun  46451  meaiuninc3v  46475  issmfle  46736  issmfgt  46747  issmfge  46761  smfpimcc  46799  smfsup  46805  smfinf  46809  2reu3  47104  2reu8i  47107  ichreuopeq  47467  reupr  47516  reuopreuprim  47520