Theorem nfralw 3311

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

Syntax hints:  Ⅎwnf 1805  Ⅎwnfc 2911  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-10 2177  ax-11 2193  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-nf 1806  df-clel 2839  df-nfc 2913  df-ral 3079

This theorem is referenced by:  rspc2  3592  sbcralt  3827  reu8nf  3832  rspc2vd  3902  raaan  4474  raaan2  4478  reusngf  4635  rexreusng  4640  reuprg0  4663  nfint  4917  nfiin  4984  disjxun  5100  nfpo  5563  nfso  5564  nffr  5622  nfse  5623  ralxpf  5820  reuop  6282  frpoinsg  6332  dff13f  7241  nfiso  7308  mpoeq123  7470  nfofr  7669  tfisg  7836  fiun  7926  f1iun  7927  fmpox  8050  ovmptss  8074  frpoins3xpg  8122  nffrecs  8266  xpf1o  9113  ac6sfi  9230  nfoi  9464  setinds  9706  frinsg  9711  scottexs  9847  scott0s  9848  lble  12146  nnwof  12917  fzrevral  13619  reuccatpfxs1  14762  rlimcld2  15607  fsum2dlem  15799  fsumcom2  15803  fprod2dlem  16012  fprodcom2  16016  gsummoncoe1  22373  cnmpt21  23733  cfilucfil  24621  ulmss  26462  fsumdvdscom  27251  dchrisumlema  27554  dchrisumlem2  27556  nosupbnd1  27780  noinfbnd1  27795  cnlnadjlem5  32276  rspc2daf  32668  disjabrex  32784  disjabrexf  32785  aciunf1lem  32866  fnpreimac  32874  fsumiunle  33033  nsgqusf1olem1  33601  ordtconnlem1  34223  esumiun  34393  bnj1366  35126  bnj1385  35129  bnj981  35247  bnj1228  35308  bnj1398  35331  bnj1445  35341  bnj1449  35345  bnj1463  35352  untsucf  36065  poimirlem26  38150  poimirlem27  38151  indexdom  38238  filbcmb  38244  sdclem1  38247  scottexf  38672  scott0f  38673  cdleme31sn1  41010  cdlemk36  41542  setindtrs  43607  oaun3lem1  43956  nfscott  44820  scottabf  44821  nfrelp  45530  modelaxrep  45562  evth2f  45600  evthf  45612  uzwo4  45638  disjinfi  45775  choicefi  45782  rnmptbd2lem  45828  rnmptbdlem  45835  ssfiunibd  45893  infxrunb2  45948  supxrunb3  45979  supxrleubrnmpt  45985  allbutfiinf  45999  suprleubrnmpt  46001  infxrgelbrnmpt  46033  caucvgbf  46068  climinff  46192  limsupre3uzlem  46314  xlimmnfv  46413  xlimpnfv  46417  cncfshift  46453  cncficcgt0  46467  stoweidlem31  46610  stoweidlem34  46613  stoweidlem35  46614  stoweidlem51  46630  stoweidlem53  46632  stoweidlem54  46633  stoweidlem57  46636  stoweidlem59  46638  stoweidlem60  46639  fourierdlem31  46717  fourierdlem73  46758  iundjiun  47039  meaiuninc3v  47063  issmfle  47324  issmfgt  47335  issmfge  47349  smfpimcc  47387  smfsup  47393  smfinf  47397  2reu3  47709  2reu8i  47712  ichreuopeq  48084  reupr  48133  reuopreuprim  48137