Theorem nfralw 3285

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876  ∀wral 3044

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 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045

This theorem is referenced by:  rspc2  3597  sbcralt  3835  reu8nf  3840  rspc2vd  3910  raaan  4480  raaan2  4484  reusngf  4638  rexreusng  4643  reuprg0  4666  nfint  4920  nfiin  4988  disjxun  5105  nfpo  5552  nfso  5553  nffr  5611  nfse  5612  ralxpf  5810  reuop  6266  frpoinsg  6316  dff13f  7230  nfiso  7297  mpoeq123  7461  nfofr  7660  tfisg  7830  fiun  7921  f1iun  7922  fmpox  8046  ovmptss  8072  frpoins3xpg  8119  nffrecs  8262  xpf1o  9103  ac6sfi  9231  nfoi  9467  frinsg  9704  scottexs  9840  scott0s  9841  lble  12135  nnwof  12873  fzrevral  13573  reuccatpfxs1  14712  rlimcld2  15544  fsum2dlem  15736  fsumcom2  15740  fprod2dlem  15946  fprodcom2  15950  gsummoncoe1  22195  cnmpt21  23558  cfilucfil  24447  ulmss  26306  fsumdvdscom  27095  dchrisumlema  27399  dchrisumlem2  27401  nosupbnd1  27626  noinfbnd1  27641  cnlnadjlem5  32000  rspc2daf  32395  disjabrex  32511  disjabrexf  32512  aciunf1lem  32586  fnpreimac  32595  fsumiunle  32754  nsgqusf1olem1  33384  ordtconnlem1  33914  esumiun  34084  bnj1366  34819  bnj1385  34822  bnj981  34940  bnj1228  35001  bnj1398  35024  bnj1445  35034  bnj1449  35038  bnj1463  35045  untsucf  35697  setinds  35766  poimirlem26  37640  poimirlem27  37641  indexdom  37728  filbcmb  37734  sdclem1  37737  scottexf  38162  scott0f  38163  cdleme31sn1  40375  cdlemk36  40907  setindtrs  43014  oaun3lem1  43363  nfscott  44228  scottabf  44229  nfrelp  44939  modelaxrep  44971  evth2f  45009  evthf  45021  uzwo4  45047  disjinfi  45186  choicefi  45194  rnmptbd2lem  45242  rnmptbdlem  45249  ssfiunibd  45307  infxrunb2  45364  supxrunb3  45395  supxrleubrnmpt  45402  allbutfiinf  45416  suprleubrnmpt  45418  infxrgelbrnmpt  45450  caucvgbf  45485  climinff  45609  limsupre3uzlem  45733  xlimmnfv  45832  xlimpnfv  45836  cncfshift  45872  cncficcgt0  45886  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem51  46049  stoweidlem53  46051  stoweidlem54  46052  stoweidlem57  46055  stoweidlem59  46057  stoweidlem60  46058  fourierdlem31  46136  fourierdlem73  46177  iundjiun  46458  meaiuninc3v  46482  issmfle  46743  issmfgt  46754  issmfge  46768  smfpimcc  46806  smfsup  46812  smfinf  46816  2reu3  47111  2reu8i  47114  ichreuopeq  47474  reupr  47523  reuopreuprim  47527