Theorem nfralw 3309

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

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-10 2138  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-clel 2811  df-nfc 2886  df-ral 3063

This theorem is referenced by:  nfra2wOLDOLD  3320  rspc2  3620  sbcralt  3866  reu8nf  3871  rspc2vd  3944  raaan  4520  raaan2  4524  reusngf  4676  rexreusng  4683  reuprg0  4706  nfint  4960  nfiin  5028  disjxun  5146  nfpo  5593  nfso  5594  nffr  5650  nfse  5651  ralxpf  5845  reuop  6290  frpoinsg  6342  wfisgOLD  6353  dff13f  7252  nfiso  7316  mpoeq123  7478  nfofr  7674  tfisg  7840  fiun  7926  f1iun  7927  fmpox  8050  ovmptss  8076  frpoins3xpg  8123  nffrecs  8265  nfwrecsOLD  8299  xpf1o  9136  ac6sfi  9284  nfoi  9506  frinsg  9743  scottexs  9879  scott0s  9880  lble  12163  nnwof  12895  fzrevral  13583  reuccatpfxs1  14694  rlimcld2  15519  fsum2dlem  15713  fsumcom2  15717  fprod2dlem  15921  fprodcom2  15925  gsummoncoe1  21820  cnmpt21  23167  cfilucfil  24060  ulmss  25901  fsumdvdscom  26679  dchrisumlema  26981  dchrisumlem2  26983  nosupbnd1  27207  noinfbnd1  27222  cnlnadjlem5  31312  rspc2daf  31696  disjabrex  31801  disjabrexf  31802  aciunf1lem  31875  fnpreimac  31884  fsumiunle  32023  nsgqusf1olem1  32513  ordtconnlem1  32893  esumiun  33081  bnj1366  33829  bnj1385  33832  bnj981  33950  bnj1228  34011  bnj1398  34034  bnj1445  34044  bnj1449  34048  bnj1463  34055  untsucf  34668  setinds  34739  poimirlem26  36503  poimirlem27  36504  indexdom  36591  filbcmb  36597  sdclem1  36600  scottexf  37025  scott0f  37026  cdleme31sn1  39241  cdlemk36  39773  setindtrs  41750  oaun3lem1  42110  nfscott  42984  scottabf  42985  evth2f  43685  evthf  43697  uzwo4  43726  disjinfi  43877  choicefi  43885  rnmptbd2lem  43939  rnmptbdlem  43946  ssfiunibd  44006  infxrunb2  44065  supxrunb3  44096  supxrleubrnmpt  44103  allbutfiinf  44117  suprleubrnmpt  44119  infxrgelbrnmpt  44151  caucvgbf  44187  climinff  44314  limsupre3uzlem  44438  xlimmnfv  44537  xlimpnfv  44541  cncfshift  44577  cncficcgt0  44591  stoweidlem31  44734  stoweidlem34  44737  stoweidlem35  44738  stoweidlem51  44754  stoweidlem53  44756  stoweidlem54  44757  stoweidlem57  44760  stoweidlem59  44762  stoweidlem60  44763  fourierdlem31  44841  fourierdlem73  44882  iundjiun  45163  meaiuninc3v  45187  issmfle  45448  issmfgt  45459  issmfge  45473  smfpimcc  45511  smfsup  45517  smfinf  45521  2reu3  45805  2reu8i  45808  ichreuopeq  46128  reupr  46177  reuopreuprim  46181