Theorem nfralw 3287

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2877  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2804  df-nfc 2879  df-ral 3046

This theorem is referenced by:  rspc2  3600  sbcralt  3838  reu8nf  3843  rspc2vd  3913  raaan  4483  raaan2  4487  reusngf  4641  rexreusng  4646  reuprg0  4669  nfint  4923  nfiin  4991  disjxun  5108  nfpo  5555  nfso  5556  nffr  5614  nfse  5615  ralxpf  5813  reuop  6269  frpoinsg  6319  dff13f  7233  nfiso  7300  mpoeq123  7464  nfofr  7663  tfisg  7833  fiun  7924  f1iun  7925  fmpox  8049  ovmptss  8075  frpoins3xpg  8122  nffrecs  8265  xpf1o  9109  ac6sfi  9238  nfoi  9474  frinsg  9711  scottexs  9847  scott0s  9848  lble  12142  nnwof  12880  fzrevral  13580  reuccatpfxs1  14719  rlimcld2  15551  fsum2dlem  15743  fsumcom2  15747  fprod2dlem  15953  fprodcom2  15957  gsummoncoe1  22202  cnmpt21  23565  cfilucfil  24454  ulmss  26313  fsumdvdscom  27102  dchrisumlema  27406  dchrisumlem2  27408  nosupbnd1  27633  noinfbnd1  27648  cnlnadjlem5  32007  rspc2daf  32402  disjabrex  32518  disjabrexf  32519  aciunf1lem  32593  fnpreimac  32602  fsumiunle  32761  nsgqusf1olem1  33391  ordtconnlem1  33921  esumiun  34091  bnj1366  34826  bnj1385  34829  bnj981  34947  bnj1228  35008  bnj1398  35031  bnj1445  35041  bnj1449  35045  bnj1463  35052  untsucf  35704  setinds  35773  poimirlem26  37647  poimirlem27  37648  indexdom  37735  filbcmb  37741  sdclem1  37744  scottexf  38169  scott0f  38170  cdleme31sn1  40382  cdlemk36  40914  setindtrs  43021  oaun3lem1  43370  nfscott  44235  scottabf  44236  nfrelp  44946  modelaxrep  44978  evth2f  45016  evthf  45028  uzwo4  45054  disjinfi  45193  choicefi  45201  rnmptbd2lem  45249  rnmptbdlem  45256  ssfiunibd  45314  infxrunb2  45371  supxrunb3  45402  supxrleubrnmpt  45409  allbutfiinf  45423  suprleubrnmpt  45425  infxrgelbrnmpt  45457  caucvgbf  45492  climinff  45616  limsupre3uzlem  45740  xlimmnfv  45839  xlimpnfv  45843  cncfshift  45879  cncficcgt0  45893  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem51  46056  stoweidlem53  46058  stoweidlem54  46059  stoweidlem57  46062  stoweidlem59  46064  stoweidlem60  46065  fourierdlem31  46143  fourierdlem73  46184  iundjiun  46465  meaiuninc3v  46489  issmfle  46750  issmfgt  46761  issmfge  46775  smfpimcc  46813  smfsup  46819  smfinf  46823  2reu3  47115  2reu8i  47118  ichreuopeq  47478  reupr  47527  reuopreuprim  47531