Theorem nfralw 3279

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2111  Ⅎwnfc 2879  ∀wral 3047

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 2113  ax-10 2144  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2806  df-nfc 2881  df-ral 3048

This theorem is referenced by:  rspc2  3581  sbcralt  3818  reu8nf  3823  rspc2vd  3893  raaan  4464  raaan2  4468  reusngf  4624  rexreusng  4629  reuprg0  4652  nfint  4905  nfiin  4972  disjxun  5087  nfpo  5528  nfso  5529  nffr  5587  nfse  5588  ralxpf  5785  reuop  6240  frpoinsg  6290  dff13f  7189  nfiso  7256  mpoeq123  7418  nfofr  7617  tfisg  7784  fiun  7875  f1iun  7876  fmpox  7999  ovmptss  8023  frpoins3xpg  8070  nffrecs  8213  xpf1o  9052  ac6sfi  9168  nfoi  9400  setinds  9639  frinsg  9644  scottexs  9780  scott0s  9781  lble  12074  nnwof  12812  fzrevral  13512  reuccatpfxs1  14654  rlimcld2  15485  fsum2dlem  15677  fsumcom2  15681  fprod2dlem  15887  fprodcom2  15891  gsummoncoe1  22223  cnmpt21  23586  cfilucfil  24474  ulmss  26333  fsumdvdscom  27122  dchrisumlema  27426  dchrisumlem2  27428  nosupbnd1  27653  noinfbnd1  27668  cnlnadjlem5  32051  rspc2daf  32445  disjabrex  32562  disjabrexf  32563  aciunf1lem  32644  fnpreimac  32653  fsumiunle  32812  nsgqusf1olem1  33378  ordtconnlem1  33937  esumiun  34107  bnj1366  34841  bnj1385  34844  bnj981  34962  bnj1228  35023  bnj1398  35046  bnj1445  35056  bnj1449  35060  bnj1463  35067  untsucf  35754  poimirlem26  37696  poimirlem27  37697  indexdom  37784  filbcmb  37790  sdclem1  37793  scottexf  38218  scott0f  38219  cdleme31sn1  40490  cdlemk36  41022  setindtrs  43128  oaun3lem1  43477  nfscott  44342  scottabf  44343  nfrelp  45052  modelaxrep  45084  evth2f  45122  evthf  45134  uzwo4  45160  disjinfi  45299  choicefi  45307  rnmptbd2lem  45355  rnmptbdlem  45362  ssfiunibd  45420  infxrunb2  45476  supxrunb3  45507  supxrleubrnmpt  45514  allbutfiinf  45528  suprleubrnmpt  45530  infxrgelbrnmpt  45562  caucvgbf  45597  climinff  45721  limsupre3uzlem  45843  xlimmnfv  45942  xlimpnfv  45946  cncfshift  45982  cncficcgt0  45996  stoweidlem31  46139  stoweidlem34  46142  stoweidlem35  46143  stoweidlem51  46159  stoweidlem53  46161  stoweidlem54  46162  stoweidlem57  46165  stoweidlem59  46167  stoweidlem60  46168  fourierdlem31  46246  fourierdlem73  46287  iundjiun  46568  meaiuninc3v  46592  issmfle  46853  issmfgt  46864  issmfge  46878  smfpimcc  46916  smfsup  46922  smfinf  46926  2reu3  47220  2reu8i  47223  ichreuopeq  47583  reupr  47632  reuopreuprim  47636