Theorem nfralw 3189

Description: Bound-variable hypothesis builder for restricted quantification. Version of nfral 3190 with a disjoint variable condition, which does not require ax-13 2379. (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 1806	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfraldw 3187	. 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1545	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1539  Ⅎwnf 1785  Ⅎwnfc 2936  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111

This theorem is referenced by:  nfra2w  3191  rspc2  3579  sbcralt  3801  reu8nf  3806  rspc2vd  3877  raaan  4418  raaan2  4422  reusngf  4572  rexreusng  4577  reuprg0  4598  nfint  4848  nfiin  4912  disjxun  5028  nfpo  5443  nfso  5444  nffr  5493  nfse  5494  ralxpf  5681  reuop  6112  wfisg  6151  dff13f  6992  nfiso  7054  mpoeq123  7205  nfofr  7395  fiun  7626  f1iun  7627  fmpox  7747  ovmptss  7771  nfwrecs  7932  xpf1o  8663  ac6sfi  8746  nfoi  8962  scottexs  9300  scott0s  9301  lble  11580  nnwof  12302  fzrevral  12987  reuccatpfxs1  14100  rlimcld2  14927  fsum2dlem  15117  fsumcom2  15121  fprod2dlem  15326  fprodcom2  15330  gsummoncoe1  20933  cnmpt21  22276  cfilucfil  23166  ulmss  24992  fsumdvdscom  25770  dchrisumlema  26072  dchrisumlem2  26074  cnlnadjlem5  29854  rspc2daf  30238  disjabrex  30345  disjabrexf  30346  aciunf1lem  30425  fnpreimac  30434  fsumiunle  30571  ordtconnlem1  31277  esumiun  31463  bnj1366  32211  bnj1385  32214  bnj981  32332  bnj1228  32393  bnj1398  32416  bnj1445  32426  bnj1449  32430  bnj1463  32437  untsucf  33049  setinds  33136  tfisg  33168  frpoinsg  33194  frinsg  33200  nffrecs  33233  nosupbnd1  33327  poimirlem26  35083  poimirlem27  35084  indexdom  35172  filbcmb  35178  sdclem1  35181  scottexf  35606  scott0f  35607  cdleme31sn1  37677  cdlemk36  38209  setindtrs  39966  nfscott  40947  scottabf  40948  evth2f  41644  evthf  41656  uzwo4  41687  disjinfi  41820  choicefi  41829  rnmptbd2lem  41886  rnmptbdlem  41893  ssfiunibd  41941  infxrunb2  42000  supxrunb3  42036  supxrleubrnmpt  42043  allbutfiinf  42057  suprleubrnmpt  42059  infxrgelbrnmpt  42093  climinff  42253  limsupre3uzlem  42377  xlimmnfv  42476  xlimpnfv  42480  cncfshift  42516  cncficcgt0  42530  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem51  42693  stoweidlem53  42695  stoweidlem54  42696  stoweidlem57  42699  stoweidlem59  42701  stoweidlem60  42702  fourierdlem31  42780  fourierdlem73  42821  iundjiun  43099  meaiuninc3v  43123  issmfle  43379  issmfgt  43390  issmfge  43403  smfpimcc  43439  smfsup  43445  smfinf  43449  2reu3  43666  2reu8i  43669  ichreuopeq  43990  reupr  44039  reuopreuprim  44043