Theorem nfralw 3317

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

Syntax hints:  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-clel 2819  df-nfc 2895  df-ral 3068

This theorem is referenced by:  nfra2wOLDOLD  3329  rspc2  3644  sbcralt  3894  reu8nf  3899  rspc2vd  3972  raaan  4540  raaan2  4544  reusngf  4696  rexreusng  4703  reuprg0  4727  nfint  4980  nfiin  5047  disjxun  5164  nfpo  5613  nfso  5614  nffr  5673  nfse  5674  ralxpf  5871  reuop  6324  frpoinsg  6375  wfisgOLD  6386  dff13f  7293  nfiso  7358  mpoeq123  7522  nfofr  7721  tfisg  7891  fiun  7983  f1iun  7984  fmpox  8108  ovmptss  8134  frpoins3xpg  8181  nffrecs  8324  nfwrecsOLD  8358  xpf1o  9205  ac6sfi  9348  nfoi  9583  frinsg  9820  scottexs  9956  scott0s  9957  lble  12247  nnwof  12979  fzrevral  13669  reuccatpfxs1  14795  rlimcld2  15624  fsum2dlem  15818  fsumcom2  15822  fprod2dlem  16028  fprodcom2  16032  gsummoncoe1  22333  cnmpt21  23700  cfilucfil  24593  ulmss  26458  fsumdvdscom  27246  dchrisumlema  27550  dchrisumlem2  27552  nosupbnd1  27777  noinfbnd1  27792  cnlnadjlem5  32103  rspc2daf  32495  disjabrex  32604  disjabrexf  32605  aciunf1lem  32680  fnpreimac  32689  fsumiunle  32833  nsgqusf1olem1  33406  ordtconnlem1  33870  esumiun  34058  bnj1366  34805  bnj1385  34808  bnj981  34926  bnj1228  34987  bnj1398  35010  bnj1445  35020  bnj1449  35024  bnj1463  35031  untsucf  35672  setinds  35742  poimirlem26  37606  poimirlem27  37607  indexdom  37694  filbcmb  37700  sdclem1  37703  scottexf  38128  scott0f  38129  cdleme31sn1  40338  cdlemk36  40870  setindtrs  42982  oaun3lem1  43336  nfscott  44208  scottabf  44209  evth2f  44915  evthf  44927  uzwo4  44955  disjinfi  45099  choicefi  45107  rnmptbd2lem  45157  rnmptbdlem  45164  ssfiunibd  45224  infxrunb2  45283  supxrunb3  45314  supxrleubrnmpt  45321  allbutfiinf  45335  suprleubrnmpt  45337  infxrgelbrnmpt  45369  caucvgbf  45405  climinff  45532  limsupre3uzlem  45656  xlimmnfv  45755  xlimpnfv  45759  cncfshift  45795  cncficcgt0  45809  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem51  45972  stoweidlem53  45974  stoweidlem54  45975  stoweidlem57  45978  stoweidlem59  45980  stoweidlem60  45981  fourierdlem31  46059  fourierdlem73  46100  iundjiun  46381  meaiuninc3v  46405  issmfle  46666  issmfgt  46677  issmfge  46691  smfpimcc  46729  smfsup  46735  smfinf  46739  2reu3  47025  2reu8i  47028  ichreuopeq  47347  reupr  47396  reuopreuprim  47400