Theorem nfralw 3291

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2883  ∀wral 3051

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 2007  ax-8 2110  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2809  df-nfc 2885  df-ral 3052

This theorem is referenced by:  rspc2  3610  sbcralt  3847  reu8nf  3852  rspc2vd  3922  raaan  4492  raaan2  4496  reusngf  4650  rexreusng  4655  reuprg0  4678  nfint  4932  nfiin  5000  disjxun  5117  nfpo  5567  nfso  5568  nffr  5627  nfse  5628  ralxpf  5826  reuop  6282  frpoinsg  6332  wfisgOLD  6343  dff13f  7248  nfiso  7315  mpoeq123  7479  nfofr  7678  tfisg  7849  fiun  7941  f1iun  7942  fmpox  8066  ovmptss  8092  frpoins3xpg  8139  nffrecs  8282  nfwrecsOLD  8316  xpf1o  9153  ac6sfi  9292  nfoi  9528  frinsg  9765  scottexs  9901  scott0s  9902  lble  12194  nnwof  12930  fzrevral  13629  reuccatpfxs1  14765  rlimcld2  15594  fsum2dlem  15786  fsumcom2  15790  fprod2dlem  15996  fprodcom2  16000  gsummoncoe1  22246  cnmpt21  23609  cfilucfil  24498  ulmss  26358  fsumdvdscom  27147  dchrisumlema  27451  dchrisumlem2  27453  nosupbnd1  27678  noinfbnd1  27693  cnlnadjlem5  32052  rspc2daf  32447  disjabrex  32563  disjabrexf  32564  aciunf1lem  32640  fnpreimac  32649  fsumiunle  32808  nsgqusf1olem1  33428  ordtconnlem1  33955  esumiun  34125  bnj1366  34860  bnj1385  34863  bnj981  34981  bnj1228  35042  bnj1398  35065  bnj1445  35075  bnj1449  35079  bnj1463  35086  untsucf  35727  setinds  35796  poimirlem26  37670  poimirlem27  37671  indexdom  37758  filbcmb  37764  sdclem1  37767  scottexf  38192  scott0f  38193  cdleme31sn1  40400  cdlemk36  40932  setindtrs  43049  oaun3lem1  43398  nfscott  44263  scottabf  44264  nfrelp  44974  modelaxrep  45006  evth2f  45039  evthf  45051  uzwo4  45077  disjinfi  45216  choicefi  45224  rnmptbd2lem  45272  rnmptbdlem  45279  ssfiunibd  45338  infxrunb2  45395  supxrunb3  45426  supxrleubrnmpt  45433  allbutfiinf  45447  suprleubrnmpt  45449  infxrgelbrnmpt  45481  caucvgbf  45516  climinff  45640  limsupre3uzlem  45764  xlimmnfv  45863  xlimpnfv  45867  cncfshift  45903  cncficcgt0  45917  stoweidlem31  46060  stoweidlem34  46063  stoweidlem35  46064  stoweidlem51  46080  stoweidlem53  46082  stoweidlem54  46083  stoweidlem57  46086  stoweidlem59  46088  stoweidlem60  46089  fourierdlem31  46167  fourierdlem73  46208  iundjiun  46489  meaiuninc3v  46513  issmfle  46774  issmfgt  46785  issmfge  46799  smfpimcc  46837  smfsup  46843  smfinf  46847  2reu3  47139  2reu8i  47142  ichreuopeq  47487  reupr  47536  reuopreuprim  47540