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  3621  sbcralt  3867  reu8nf  3872  rspc2vd  3945  raaan  4521  raaan2  4525  reusngf  4677  rexreusng  4684  reuprg0  4707  nfint  4961  nfiin  5029  disjxun  5147  nfpo  5594  nfso  5595  nffr  5651  nfse  5652  ralxpf  5847  reuop  6293  frpoinsg  6345  wfisgOLD  6356  dff13f  7255  nfiso  7319  mpoeq123  7481  nfofr  7677  tfisg  7843  fiun  7929  f1iun  7930  fmpox  8053  ovmptss  8079  frpoins3xpg  8126  nffrecs  8268  nfwrecsOLD  8302  xpf1o  9139  ac6sfi  9287  nfoi  9509  frinsg  9746  scottexs  9882  scott0s  9883  lble  12166  nnwof  12898  fzrevral  13586  reuccatpfxs1  14697  rlimcld2  15522  fsum2dlem  15716  fsumcom2  15720  fprod2dlem  15924  fprodcom2  15928  gsummoncoe1  21828  cnmpt21  23175  cfilucfil  24068  ulmss  25909  fsumdvdscom  26689  dchrisumlema  26991  dchrisumlem2  26993  nosupbnd1  27217  noinfbnd1  27232  cnlnadjlem5  31355  rspc2daf  31739  disjabrex  31844  disjabrexf  31845  aciunf1lem  31918  fnpreimac  31927  fsumiunle  32066  nsgqusf1olem1  32555  ordtconnlem1  32935  esumiun  33123  bnj1366  33871  bnj1385  33874  bnj981  33992  bnj1228  34053  bnj1398  34076  bnj1445  34086  bnj1449  34090  bnj1463  34097  untsucf  34710  setinds  34781  poimirlem26  36562  poimirlem27  36563  indexdom  36650  filbcmb  36656  sdclem1  36659  scottexf  37084  scott0f  37085  cdleme31sn1  39300  cdlemk36  39832  setindtrs  41812  oaun3lem1  42172  nfscott  43046  scottabf  43047  evth2f  43747  evthf  43759  uzwo4  43788  disjinfi  43939  choicefi  43947  rnmptbd2lem  44000  rnmptbdlem  44007  ssfiunibd  44067  infxrunb2  44126  supxrunb3  44157  supxrleubrnmpt  44164  allbutfiinf  44178  suprleubrnmpt  44180  infxrgelbrnmpt  44212  caucvgbf  44248  climinff  44375  limsupre3uzlem  44499  xlimmnfv  44598  xlimpnfv  44602  cncfshift  44638  cncficcgt0  44652  stoweidlem31  44795  stoweidlem34  44798  stoweidlem35  44799  stoweidlem51  44815  stoweidlem53  44817  stoweidlem54  44818  stoweidlem57  44821  stoweidlem59  44823  stoweidlem60  44824  fourierdlem31  44902  fourierdlem73  44943  iundjiun  45224  meaiuninc3v  45248  issmfle  45509  issmfgt  45520  issmfge  45534  smfpimcc  45572  smfsup  45578  smfinf  45582  2reu3  45866  2reu8i  45869  ichreuopeq  46189  reupr  46238  reuopreuprim  46242