Theorem nfralw 3318

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

Syntax hints:  Ⅎwnf 1810  Ⅎwnfc 2916  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-10 2182  ax-11 2198  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-clel 2844  df-nfc 2918  df-ral 3086

This theorem is referenced by:  rspc2  3599  sbcralt  3834  reu8nf  3839  rspc2vd  3909  raaan  4484  raaan2  4488  reusngf  4645  rexreusng  4650  reuprg0  4673  nfint  4926  nfiin  4993  disjxun  5111  nfpo  5576  nfso  5577  nffr  5635  nfse  5636  ralxpf  5833  reuop  6295  frpoinsg  6345  dff13f  7254  nfiso  7321  mpoeq123  7483  nfofr  7682  tfisg  7850  fiun  7940  f1iun  7941  fmpox  8064  ovmptss  8088  frpoins3xpg  8136  nffrecs  8280  xpf1o  9127  ac6sfi  9244  nfoi  9476  setinds  9718  frinsg  9723  scottexs  9861  scott0s  9862  nfscott  9865  scottabf  9866  lble  12167  nnwof  12938  fzrevral  13640  reuccatpfxs1  14784  rlimcld2  15629  fsum2dlem  15821  fsumcom2  15825  fprod2dlem  16034  fprodcom2  16038  gsummoncoe1  22437  cnmpt21  23797  cfilucfil  24685  ulmss  26526  fsumdvdscom  27315  dchrisumlema  27618  dchrisumlem2  27620  nosupbnd1  27844  noinfbnd1  27859  cnlnadjlem5  32364  rspc2daf  32754  disjabrex  32868  disjabrexf  32869  aciunf1lem  32948  fnpreimac  32956  fsumiunle  33114  nsgqusf1olem1  33666  ordtconnlem1  34259  esumiun  34429  bnj1366  35162  bnj1385  35165  bnj981  35283  bnj1228  35344  bnj1398  35367  bnj1445  35377  bnj1449  35381  bnj1463  35388  untsucf  36135  poimirlem26  38219  poimirlem27  38220  indexdom  38307  filbcmb  38313  sdclem1  38316  scottexf  38741  scott0f  38742  cdleme31sn1  41079  cdlemk36  41611  setindtrs  43678  oaun3lem1  44027  nfrelp  45584  modelaxrep  45616  evth2f  45661  evthf  45673  uzwo4  45699  disjinfi  45836  choicefi  45843  rnmptbd2lem  45889  rnmptbdlem  45896  ssfiunibd  45954  infxrunb2  46009  supxrunb3  46040  supxrleubrnmpt  46046  allbutfiinf  46060  suprleubrnmpt  46062  infxrgelbrnmpt  46094  caucvgbf  46129  climinff  46253  limsupre3uzlem  46375  xlimmnfv  46474  xlimpnfv  46478  cncfshift  46514  cncficcgt0  46528  stoweidlem31  46671  stoweidlem34  46674  stoweidlem35  46675  stoweidlem51  46691  stoweidlem53  46693  stoweidlem54  46694  stoweidlem57  46697  stoweidlem59  46699  stoweidlem60  46700  fourierdlem31  46778  fourierdlem73  46819  iundjiun  47100  meaiuninc3v  47124  issmfle  47385  issmfgt  47396  issmfge  47410  smfpimcc  47448  smfsup  47454  smfinf  47458  2reu3  47770  2reu8i  47773  ichreuopeq  48145  reupr  48194  reuopreuprim  48198  nfrals  50501