Theorem nfralw 3283

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3345 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 3280	. 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  3594  sbcralt  3832  reu8nf  3837  rspc2vd  3907  raaan  4476  raaan2  4480  reusngf  4634  rexreusng  4639  reuprg0  4662  nfint  4916  nfiin  4984  disjxun  5100  nfpo  5545  nfso  5546  nffr  5604  nfse  5605  ralxpf  5800  reuop  6254  frpoinsg  6304  dff13f  7212  nfiso  7279  mpoeq123  7441  nfofr  7640  tfisg  7810  fiun  7901  f1iun  7902  fmpox  8025  ovmptss  8049  frpoins3xpg  8096  nffrecs  8239  xpf1o  9080  ac6sfi  9207  nfoi  9443  frinsg  9680  scottexs  9816  scott0s  9817  lble  12111  nnwof  12849  fzrevral  13549  reuccatpfxs1  14688  rlimcld2  15520  fsum2dlem  15712  fsumcom2  15716  fprod2dlem  15922  fprodcom2  15926  gsummoncoe1  22228  cnmpt21  23591  cfilucfil  24480  ulmss  26339  fsumdvdscom  27128  dchrisumlema  27432  dchrisumlem2  27434  nosupbnd1  27659  noinfbnd1  27674  cnlnadjlem5  32050  rspc2daf  32445  disjabrex  32561  disjabrexf  32562  aciunf1lem  32636  fnpreimac  32645  fsumiunle  32804  nsgqusf1olem1  33377  ordtconnlem1  33907  esumiun  34077  bnj1366  34812  bnj1385  34815  bnj981  34933  bnj1228  34994  bnj1398  35017  bnj1445  35027  bnj1449  35031  bnj1463  35038  untsucf  35690  setinds  35759  poimirlem26  37633  poimirlem27  37634  indexdom  37721  filbcmb  37727  sdclem1  37730  scottexf  38155  scott0f  38156  cdleme31sn1  40368  cdlemk36  40900  setindtrs  43007  oaun3lem1  43356  nfscott  44221  scottabf  44222  nfrelp  44932  modelaxrep  44964  evth2f  45002  evthf  45014  uzwo4  45040  disjinfi  45179  choicefi  45187  rnmptbd2lem  45235  rnmptbdlem  45242  ssfiunibd  45300  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