Theorem nfralw 3225

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3226 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 1-Sep-1999.) (Revised by Gino Giotto, 10-Jan-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		nftru 1805	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfraldw 3223	. 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1544	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1784  Ⅎwnfc 2961  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143

This theorem is referenced by:  nfra2w  3227  rspc2  3631  sbcralt  3855  reu8nf  3860  rspc2vd  3932  raaan  4460  raaan2  4464  reusngf  4612  rexreusng  4617  reuprg0  4638  nfint  4886  nfiin  4950  disjxun  5064  nfpo  5479  nfso  5480  nffr  5529  nfse  5530  ralxpf  5717  reuop  6144  wfisg  6183  dff13f  7014  nfiso  7075  mpoeq123  7226  nfofr  7415  fiun  7644  f1iun  7645  fmpox  7765  ovmptss  7788  nfwrecs  7949  xpf1o  8679  ac6sfi  8762  nfoi  8978  scottexs  9316  scott0s  9317  lble  11593  nnwof  12315  fzrevral  12993  reuccatpfxs1  14109  rlimcld2  14935  fsum2dlem  15125  fsumcom2  15129  fprod2dlem  15334  fprodcom2  15338  gsummoncoe1  20472  cnmpt21  22279  cfilucfil  23169  ulmss  24985  fsumdvdscom  25762  dchrisumlema  26064  dchrisumlem2  26066  cnlnadjlem5  29848  rspc2daf  30231  disjabrex  30332  disjabrexf  30333  aciunf1lem  30407  fnpreimac  30416  fsumiunle  30545  ordtconnlem1  31167  esumiun  31353  bnj1366  32101  bnj1385  32104  bnj981  32222  bnj1228  32283  bnj1398  32306  bnj1445  32316  bnj1449  32320  bnj1463  32327  untsucf  32936  setinds  33023  tfisg  33055  frpoinsg  33081  frinsg  33087  nffrecs  33120  nosupbnd1  33214  poimirlem26  34933  poimirlem27  34934  indexdom  35024  filbcmb  35030  sdclem1  35033  scottexf  35461  scott0f  35462  cdleme31sn1  37532  cdlemk36  38064  setindtrs  39671  nfscott  40624  scottabf  40625  evth2f  41321  evthf  41333  uzwo4  41364  disjinfi  41503  choicefi  41512  rnmptbd2lem  41569  rnmptbdlem  41576  ssfiunibd  41625  infxrunb2  41685  supxrunb3  41721  supxrleubrnmpt  41728  allbutfiinf  41743  suprleubrnmpt  41745  infxrgelbrnmpt  41779  climinff  41941  limsupre3uzlem  42065  xlimmnfv  42164  xlimpnfv  42168  cncfshift  42206  cncficcgt0  42220  stoweidlem31  42365  stoweidlem34  42368  stoweidlem35  42369  stoweidlem51  42385  stoweidlem53  42387  stoweidlem54  42388  stoweidlem57  42391  stoweidlem59  42393  stoweidlem60  42394  fourierdlem31  42472  fourierdlem73  42513  iundjiun  42791  meaiuninc3v  42815  issmfle  43071  issmfgt  43082  issmfge  43095  smfpimcc  43131  smfsup  43137  smfinf  43141  2reu3  43358  2reu8i  43361  ichreuopeq  43684  reupr  43733  reuopreuprim  43737