Theorem nfralw 3307

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2105  Ⅎwnfc 2882  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-10 2136  ax-11 2153  ax-12 2170

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-nf 1785  df-clel 2809  df-nfc 2884  df-ral 3061

This theorem is referenced by:  nfra2wOLDOLD  3318  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  5846  reuop  6292  frpoinsg  6344  wfisgOLD  6355  dff13f  7258  nfiso  7322  mpoeq123  7484  nfofr  7681  tfisg  7847  fiun  7933  f1iun  7934  fmpox  8057  ovmptss  8084  frpoins3xpg  8131  nffrecs  8274  nfwrecsOLD  8308  xpf1o  9145  ac6sfi  9293  nfoi  9515  frinsg  9752  scottexs  9888  scott0s  9889  lble  12173  nnwof  12905  fzrevral  13593  reuccatpfxs1  14704  rlimcld2  15529  fsum2dlem  15723  fsumcom2  15727  fprod2dlem  15931  fprodcom2  15935  gsummoncoe1  22148  cnmpt21  23495  cfilucfil  24388  ulmss  26248  fsumdvdscom  27030  dchrisumlema  27334  dchrisumlem2  27336  nosupbnd1  27560  noinfbnd1  27575  cnlnadjlem5  31757  rspc2daf  32141  disjabrex  32246  disjabrexf  32247  aciunf1lem  32320  fnpreimac  32329  fsumiunle  32468  nsgqusf1olem1  32964  ordtconnlem1  33368  esumiun  33556  bnj1366  34304  bnj1385  34307  bnj981  34425  bnj1228  34486  bnj1398  34509  bnj1445  34519  bnj1449  34523  bnj1463  34530  untsucf  35149  setinds  35220  poimirlem26  36978  poimirlem27  36979  indexdom  37066  filbcmb  37072  sdclem1  37075  scottexf  37500  scott0f  37501  cdleme31sn1  39716  cdlemk36  40248  setindtrs  42227  oaun3lem1  42587  nfscott  43461  scottabf  43462  evth2f  44162  evthf  44174  uzwo4  44202  disjinfi  44350  choicefi  44358  rnmptbd2lem  44411  rnmptbdlem  44418  ssfiunibd  44478  infxrunb2  44537  supxrunb3  44568  supxrleubrnmpt  44575  allbutfiinf  44589  suprleubrnmpt  44591  infxrgelbrnmpt  44623  caucvgbf  44659  climinff  44786  limsupre3uzlem  44910  xlimmnfv  45009  xlimpnfv  45013  cncfshift  45049  cncficcgt0  45063  stoweidlem31  45206  stoweidlem34  45209  stoweidlem35  45210  stoweidlem51  45226  stoweidlem53  45228  stoweidlem54  45229  stoweidlem57  45232  stoweidlem59  45234  stoweidlem60  45235  fourierdlem31  45313  fourierdlem73  45354  iundjiun  45635  meaiuninc3v  45659  issmfle  45920  issmfgt  45931  issmfge  45945  smfpimcc  45983  smfsup  45989  smfinf  45993  2reu3  46277  2reu8i  46280  ichreuopeq  46600  reupr  46649  reuopreuprim  46653