Theorem nfralw 3281

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2881  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-10 2146  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2809  df-nfc 2883  df-ral 3050

This theorem is referenced by:  rspc2  3583  sbcralt  3820  reu8nf  3825  rspc2vd  3895  raaan  4469  raaan2  4473  reusngf  4629  rexreusng  4634  reuprg0  4657  nfint  4910  nfiin  4977  disjxun  5094  nfpo  5536  nfso  5537  nffr  5595  nfse  5596  ralxpf  5793  reuop  6249  frpoinsg  6299  dff13f  7199  nfiso  7266  mpoeq123  7428  nfofr  7627  tfisg  7794  fiun  7885  f1iun  7886  fmpox  8009  ovmptss  8033  frpoins3xpg  8080  nffrecs  8223  xpf1o  9065  ac6sfi  9182  nfoi  9417  setinds  9656  frinsg  9661  scottexs  9797  scott0s  9798  lble  12092  nnwof  12825  fzrevral  13526  reuccatpfxs1  14668  rlimcld2  15499  fsum2dlem  15691  fsumcom2  15695  fprod2dlem  15901  fprodcom2  15905  gsummoncoe1  22250  cnmpt21  23613  cfilucfil  24501  ulmss  26360  fsumdvdscom  27149  dchrisumlema  27453  dchrisumlem2  27455  nosupbnd1  27680  noinfbnd1  27695  cnlnadjlem5  32095  rspc2daf  32489  disjabrex  32606  disjabrexf  32607  aciunf1lem  32689  fnpreimac  32698  fsumiunle  32859  nsgqusf1olem1  33443  ordtconnlem1  34030  esumiun  34200  bnj1366  34934  bnj1385  34937  bnj981  35055  bnj1228  35116  bnj1398  35139  bnj1445  35149  bnj1449  35153  bnj1463  35160  untsucf  35853  poimirlem26  37786  poimirlem27  37787  indexdom  37874  filbcmb  37880  sdclem1  37883  scottexf  38308  scott0f  38309  cdleme31sn1  40580  cdlemk36  41112  setindtrs  43209  oaun3lem1  43558  nfscott  44422  scottabf  44423  nfrelp  45132  modelaxrep  45164  evth2f  45202  evthf  45214  uzwo4  45240  disjinfi  45378  choicefi  45386  rnmptbd2lem  45434  rnmptbdlem  45441  ssfiunibd  45499  infxrunb2  45554  supxrunb3  45585  supxrleubrnmpt  45592  allbutfiinf  45606  suprleubrnmpt  45608  infxrgelbrnmpt  45640  caucvgbf  45675  climinff  45799  limsupre3uzlem  45921  xlimmnfv  46020  xlimpnfv  46024  cncfshift  46060  cncficcgt0  46074  stoweidlem31  46217  stoweidlem34  46220  stoweidlem35  46221  stoweidlem51  46237  stoweidlem53  46239  stoweidlem54  46240  stoweidlem57  46243  stoweidlem59  46245  stoweidlem60  46246  fourierdlem31  46324  fourierdlem73  46365  iundjiun  46646  meaiuninc3v  46670  issmfle  46931  issmfgt  46942  issmfge  46956  smfpimcc  46994  smfsup  47000  smfinf  47004  2reu3  47298  2reu8i  47301  ichreuopeq  47661  reupr  47710  reuopreuprim  47714