Theorem nfralw 3285

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3346 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 3282	. 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  3587  sbcralt  3824  reu8nf  3829  rspc2vd  3899  raaan  4473  raaan2  4477  reusngf  4633  rexreusng  4638  reuprg0  4661  nfint  4914  nfiin  4981  disjxun  5098  nfpo  5548  nfso  5549  nffr  5607  nfse  5608  ralxpf  5805  reuop  6261  frpoinsg  6311  dff13f  7213  nfiso  7280  mpoeq123  7442  nfofr  7641  tfisg  7808  fiun  7899  f1iun  7900  fmpox  8023  ovmptss  8047  frpoins3xpg  8094  nffrecs  8237  xpf1o  9081  ac6sfi  9198  nfoi  9433  setinds  9672  frinsg  9677  scottexs  9813  scott0s  9814  lble  12108  nnwof  12841  fzrevral  13542  reuccatpfxs1  14684  rlimcld2  15515  fsum2dlem  15707  fsumcom2  15711  fprod2dlem  15917  fprodcom2  15921  gsummoncoe1  22269  cnmpt21  23632  cfilucfil  24520  ulmss  26379  fsumdvdscom  27168  dchrisumlema  27472  dchrisumlem2  27474  nosupbnd1  27699  noinfbnd1  27714  cnlnadjlem5  32165  rspc2daf  32558  disjabrex  32675  disjabrexf  32676  aciunf1lem  32758  fnpreimac  32766  fsumiunle  32927  nsgqusf1olem1  33512  ordtconnlem1  34108  esumiun  34278  bnj1366  35011  bnj1385  35014  bnj981  35132  bnj1228  35193  bnj1398  35216  bnj1445  35226  bnj1449  35230  bnj1463  35237  untsucf  35932  poimirlem26  37926  poimirlem27  37927  indexdom  38014  filbcmb  38020  sdclem1  38023  scottexf  38448  scott0f  38449  cdleme31sn1  40786  cdlemk36  41318  setindtrs  43411  oaun3lem1  43760  nfscott  44624  scottabf  44625  nfrelp  45334  modelaxrep  45366  evth2f  45404  evthf  45416  uzwo4  45442  disjinfi  45580  choicefi  45587  rnmptbd2lem  45635  rnmptbdlem  45642  ssfiunibd  45700  infxrunb2  45755  supxrunb3  45786  supxrleubrnmpt  45793  allbutfiinf  45807  suprleubrnmpt  45809  infxrgelbrnmpt  45841  caucvgbf  45876  climinff  46000  limsupre3uzlem  46122  xlimmnfv  46221  xlimpnfv  46225  cncfshift  46261  cncficcgt0  46275  stoweidlem31  46418  stoweidlem34  46421  stoweidlem35  46422  stoweidlem51  46438  stoweidlem53  46440  stoweidlem54  46441  stoweidlem57  46444  stoweidlem59  46446  stoweidlem60  46447  fourierdlem31  46525  fourierdlem73  46566  iundjiun  46847  meaiuninc3v  46871  issmfle  47132  issmfgt  47143  issmfge  47157  smfpimcc  47195  smfsup  47201  smfinf  47205  2reu3  47499  2reu8i  47502  ichreuopeq  47862  reupr  47911  reuopreuprim  47915