Theorem nfralw 3284

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3345 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 2891	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
3	2	nf5ri 2203	. . 3 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	nf5ri 2203	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
6	3, 5	hbral 3281	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	nf5i 2152	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053

This theorem is referenced by:  rspc2  3586  sbcralt  3823  reu8nf  3828  rspc2vd  3898  raaan  4472  raaan2  4476  reusngf  4632  rexreusng  4637  reuprg0  4660  nfint  4913  nfiin  4980  disjxun  5097  nfpo  5539  nfso  5540  nffr  5598  nfse  5599  ralxpf  5796  reuop  6252  frpoinsg  6302  dff13f  7203  nfiso  7270  mpoeq123  7432  nfofr  7631  tfisg  7798  fiun  7889  f1iun  7890  fmpox  8013  ovmptss  8037  frpoins3xpg  8084  nffrecs  8227  xpf1o  9071  ac6sfi  9188  nfoi  9423  setinds  9662  frinsg  9667  scottexs  9803  scott0s  9804  lble  12098  nnwof  12831  fzrevral  13532  reuccatpfxs1  14674  rlimcld2  15505  fsum2dlem  15697  fsumcom2  15701  fprod2dlem  15907  fprodcom2  15911  gsummoncoe1  22256  cnmpt21  23619  cfilucfil  24507  ulmss  26366  fsumdvdscom  27155  dchrisumlema  27459  dchrisumlem2  27461  nosupbnd1  27686  noinfbnd1  27701  cnlnadjlem5  32150  rspc2daf  32543  disjabrex  32660  disjabrexf  32661  aciunf1lem  32743  fnpreimac  32751  fsumiunle  32912  nsgqusf1olem1  33496  ordtconnlem1  34083  esumiun  34253  bnj1366  34987  bnj1385  34990  bnj981  35108  bnj1228  35169  bnj1398  35192  bnj1445  35202  bnj1449  35206  bnj1463  35213  untsucf  35906  poimirlem26  37849  poimirlem27  37850  indexdom  37937  filbcmb  37943  sdclem1  37946  scottexf  38371  scott0f  38372  cdleme31sn1  40709  cdlemk36  41241  setindtrs  43334  oaun3lem1  43683  nfscott  44547  scottabf  44548  nfrelp  45257  modelaxrep  45289  evth2f  45327  evthf  45339  uzwo4  45365  disjinfi  45503  choicefi  45511  rnmptbd2lem  45559  rnmptbdlem  45566  ssfiunibd  45624  infxrunb2  45679  supxrunb3  45710  supxrleubrnmpt  45717  allbutfiinf  45731  suprleubrnmpt  45733  infxrgelbrnmpt  45765  caucvgbf  45800  climinff  45924  limsupre3uzlem  46046  xlimmnfv  46145  xlimpnfv  46149  cncfshift  46185  cncficcgt0  46199  stoweidlem31  46342  stoweidlem34  46345  stoweidlem35  46346  stoweidlem51  46362  stoweidlem53  46364  stoweidlem54  46365  stoweidlem57  46368  stoweidlem59  46370  stoweidlem60  46371  fourierdlem31  46449  fourierdlem73  46490  iundjiun  46771  meaiuninc3v  46795  issmfle  47056  issmfgt  47067  issmfge  47081  smfpimcc  47119  smfsup  47125  smfinf  47129  2reu3  47423  2reu8i  47426  ichreuopeq  47786  reupr  47835  reuopreuprim  47839