Theorem nfralw 3288

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

Syntax hints:  Ⅎwnf 1791  Ⅎwnfc 2888  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-10 2154  ax-11 2170  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-nf 1792  df-clel 2816  df-nfc 2890  df-ral 3056

This theorem is referenced by:  rspc2  3571  sbcralt  3806  reu8nf  3811  rspc2vd  3881  raaan  4449  raaan2  4453  reusngf  4609  rexreusng  4614  reuprg0  4637  nfint  4890  nfiin  4957  disjxun  5073  nfpo  5535  nfso  5536  nffr  5594  nfse  5595  ralxpf  5791  reuop  6248  frpoinsg  6298  dff13f  7203  nfiso  7270  mpoeq123  7432  nfofr  7631  tfisg  7798  fiun  7889  f1iun  7890  fmpox  8013  ovmptss  8036  frpoins3xpg  8084  nffrecs  8227  xpf1o  9071  ac6sfi  9188  nfoi  9423  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  22298  cnmpt21  23658  cfilucfil  24546  ulmss  26384  fsumdvdscom  27170  dchrisumlema  27473  dchrisumlem2  27475  nosupbnd1  27700  noinfbnd1  27715  cnlnadjlem5  32164  rspc2daf  32557  disjabrex  32675  disjabrexf  32676  aciunf1lem  32758  fnpreimac  32766  fsumiunle  32925  nsgqusf1olem1  33500  ordtconnlem1  34120  esumiun  34290  bnj1366  35026  bnj1385  35029  bnj981  35147  bnj1228  35208  bnj1398  35231  bnj1445  35241  bnj1449  35245  bnj1463  35252  untsucf  35953  poimirlem26  38028  poimirlem27  38029  indexdom  38116  filbcmb  38122  sdclem1  38125  scottexf  38550  scott0f  38551  cdleme31sn1  40888  cdlemk36  41420  setindtrs  43485  oaun3lem1  43834  nfscott  44698  scottabf  44699  nfrelp  45408  modelaxrep  45440  evth2f  45478  evthf  45490  uzwo4  45516  disjinfi  45653  choicefi  45660  rnmptbd2lem  45706  rnmptbdlem  45713  ssfiunibd  45771  infxrunb2  45826  supxrunb3  45857  supxrleubrnmpt  45863  allbutfiinf  45877  suprleubrnmpt  45879  infxrgelbrnmpt  45911  caucvgbf  45946  climinff  46070  limsupre3uzlem  46192  xlimmnfv  46291  xlimpnfv  46295  cncfshift  46331  cncficcgt0  46345  stoweidlem31  46488  stoweidlem34  46491  stoweidlem35  46492  stoweidlem51  46508  stoweidlem53  46510  stoweidlem54  46511  stoweidlem57  46514  stoweidlem59  46516  stoweidlem60  46517  fourierdlem31  46595  fourierdlem73  46636  iundjiun  46917  meaiuninc3v  46941  issmfle  47202  issmfgt  47213  issmfge  47227  smfpimcc  47265  smfsup  47271  smfinf  47275  2reu3  47587  2reu8i  47590  ichreuopeq  47962  reupr  48011  reuopreuprim  48015