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  39642  nfscott  40595  scottabf  40596  evth2f  41292  evthf  41304  uzwo4  41335  disjinfi  41474  choicefi  41483  rnmptbd2lem  41540  rnmptbdlem  41547  ssfiunibd  41596  infxrunb2  41656  supxrunb3  41692  supxrleubrnmpt  41699  allbutfiinf  41714  suprleubrnmpt  41716  infxrgelbrnmpt  41750  climinff  41912  limsupre3uzlem  42036  xlimmnfv  42135  xlimpnfv  42139  cncfshift  42177  cncficcgt0  42191  stoweidlem31  42336  stoweidlem34  42339  stoweidlem35  42340  stoweidlem51  42356  stoweidlem53  42358  stoweidlem54  42359  stoweidlem57  42362  stoweidlem59  42364  stoweidlem60  42365  fourierdlem31  42443  fourierdlem73  42484  iundjiun  42762  meaiuninc3v  42786  issmfle  43042  issmfgt  43053  issmfge  43066  smfpimcc  43102  smfsup  43108  smfinf  43112  2reu3  43329  2reu8i  43332  ichreuopeq  43655  reupr  43704  reuopreuprim  43708