Theorem nfralw 3285

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

Syntax hints:  Ⅎwnf 1785  Ⅎwnfc 2884  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053

This theorem is referenced by:  rspc2  3574  sbcralt  3811  reu8nf  3816  rspc2vd  3886  raaan  4459  raaan2  4463  reusngf  4619  rexreusng  4624  reuprg0  4647  nfint  4900  nfiin  4967  disjxun  5084  nfpo  5540  nfso  5541  nffr  5599  nfse  5600  ralxpf  5797  reuop  6253  frpoinsg  6303  dff13f  7205  nfiso  7272  mpoeq123  7434  nfofr  7633  tfisg  7800  fiun  7891  f1iun  7892  fmpox  8015  ovmptss  8038  frpoins3xpg  8085  nffrecs  8228  xpf1o  9072  ac6sfi  9189  nfoi  9424  setinds  9665  frinsg  9670  scottexs  9806  scott0s  9807  lble  12103  nnwof  12859  fzrevral  13561  reuccatpfxs1  14704  rlimcld2  15535  fsum2dlem  15727  fsumcom2  15731  fprod2dlem  15940  fprodcom2  15944  gsummoncoe1  22287  cnmpt21  23650  cfilucfil  24538  ulmss  26379  fsumdvdscom  27166  dchrisumlema  27469  dchrisumlem2  27471  nosupbnd1  27696  noinfbnd1  27711  cnlnadjlem5  32161  rspc2daf  32554  disjabrex  32671  disjabrexf  32672  aciunf1lem  32754  fnpreimac  32762  fsumiunle  32921  nsgqusf1olem1  33492  ordtconnlem1  34088  esumiun  34258  bnj1366  34991  bnj1385  34994  bnj981  35112  bnj1228  35173  bnj1398  35196  bnj1445  35206  bnj1449  35210  bnj1463  35217  untsucf  35912  poimirlem26  37985  poimirlem27  37986  indexdom  38073  filbcmb  38079  sdclem1  38082  scottexf  38507  scott0f  38508  cdleme31sn1  40845  cdlemk36  41377  setindtrs  43475  oaun3lem1  43824  nfscott  44688  scottabf  44689  nfrelp  45398  modelaxrep  45430  evth2f  45468  evthf  45480  uzwo4  45506  disjinfi  45644  choicefi  45651  rnmptbd2lem  45699  rnmptbdlem  45706  ssfiunibd  45764  infxrunb2  45819  supxrunb3  45850  supxrleubrnmpt  45856  allbutfiinf  45870  suprleubrnmpt  45872  infxrgelbrnmpt  45904  caucvgbf  45939  climinff  46063  limsupre3uzlem  46185  xlimmnfv  46284  xlimpnfv  46288  cncfshift  46324  cncficcgt0  46338  stoweidlem31  46481  stoweidlem34  46484  stoweidlem35  46485  stoweidlem51  46501  stoweidlem53  46503  stoweidlem54  46504  stoweidlem57  46507  stoweidlem59  46509  stoweidlem60  46510  fourierdlem31  46588  fourierdlem73  46629  iundjiun  46910  meaiuninc3v  46934  issmfle  47195  issmfgt  47206  issmfge  47220  smfpimcc  47258  smfsup  47264  smfinf  47268  2reu3  47574  2reu8i  47577  ichreuopeq  47949  reupr  47998  reuopreuprim  48002