Theorem nfralw 3311

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2890  ∀wral 3061

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 2007  ax-8 2110  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062

This theorem is referenced by:  rspc2  3631  sbcralt  3872  reu8nf  3877  rspc2vd  3947  raaan  4517  raaan2  4521  reusngf  4674  rexreusng  4679  reuprg0  4702  nfint  4956  nfiin  5024  disjxun  5141  nfpo  5598  nfso  5599  nffr  5658  nfse  5659  ralxpf  5857  reuop  6313  frpoinsg  6364  wfisgOLD  6375  dff13f  7276  nfiso  7342  mpoeq123  7505  nfofr  7704  tfisg  7875  fiun  7967  f1iun  7968  fmpox  8092  ovmptss  8118  frpoins3xpg  8165  nffrecs  8308  nfwrecsOLD  8342  xpf1o  9179  ac6sfi  9320  nfoi  9554  frinsg  9791  scottexs  9927  scott0s  9928  lble  12220  nnwof  12956  fzrevral  13652  reuccatpfxs1  14785  rlimcld2  15614  fsum2dlem  15806  fsumcom2  15810  fprod2dlem  16016  fprodcom2  16020  gsummoncoe1  22312  cnmpt21  23679  cfilucfil  24572  ulmss  26440  fsumdvdscom  27228  dchrisumlema  27532  dchrisumlem2  27534  nosupbnd1  27759  noinfbnd1  27774  cnlnadjlem5  32090  rspc2daf  32485  disjabrex  32595  disjabrexf  32596  aciunf1lem  32672  fnpreimac  32681  fsumiunle  32831  nsgqusf1olem1  33441  ordtconnlem1  33923  esumiun  34095  bnj1366  34843  bnj1385  34846  bnj981  34964  bnj1228  35025  bnj1398  35048  bnj1445  35058  bnj1449  35062  bnj1463  35069  untsucf  35710  setinds  35779  poimirlem26  37653  poimirlem27  37654  indexdom  37741  filbcmb  37747  sdclem1  37750  scottexf  38175  scott0f  38176  cdleme31sn1  40383  cdlemk36  40915  setindtrs  43037  oaun3lem1  43387  nfscott  44258  scottabf  44259  nfrelp  44970  modelaxrep  44998  evth2f  45020  evthf  45032  uzwo4  45058  disjinfi  45197  choicefi  45205  rnmptbd2lem  45255  rnmptbdlem  45262  ssfiunibd  45321  infxrunb2  45379  supxrunb3  45410  supxrleubrnmpt  45417  allbutfiinf  45431  suprleubrnmpt  45433  infxrgelbrnmpt  45465  caucvgbf  45500  climinff  45626  limsupre3uzlem  45750  xlimmnfv  45849  xlimpnfv  45853  cncfshift  45889  cncficcgt0  45903  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem51  46066  stoweidlem53  46068  stoweidlem54  46069  stoweidlem57  46072  stoweidlem59  46074  stoweidlem60  46075  fourierdlem31  46153  fourierdlem73  46194  iundjiun  46475  meaiuninc3v  46499  issmfle  46760  issmfgt  46771  issmfge  46785  smfpimcc  46823  smfsup  46829  smfinf  46833  2reu3  47122  2reu8i  47125  ichreuopeq  47460  reupr  47509  reuopreuprim  47513