Theorem nfralw 3151

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

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2106  Ⅎwnfc 2887  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-clel 2816  df-nfc 2889  df-ral 3069

This theorem is referenced by:  nfra2wOLDOLD  3156  rspc2  3568  sbcralt  3805  reu8nf  3810  rspc2vd  3883  raaan  4451  raaan2  4455  reusngf  4608  rexreusng  4615  reuprg0  4638  nfint  4889  nfiin  4955  disjxun  5072  nfpo  5508  nfso  5509  nffr  5563  nfse  5564  ralxpf  5755  reuop  6196  frpoinsg  6246  wfisgOLD  6257  dff13f  7129  nfiso  7193  mpoeq123  7347  nfofr  7540  fiun  7785  f1iun  7786  fmpox  7907  ovmptss  7933  nffrecs  8099  nfwrecsOLD  8133  xpf1o  8926  ac6sfi  9058  nfoi  9273  frinsg  9509  scottexs  9645  scott0s  9646  lble  11927  nnwof  12654  fzrevral  13341  reuccatpfxs1  14460  rlimcld2  15287  fsum2dlem  15482  fsumcom2  15486  fprod2dlem  15690  fprodcom2  15694  gsummoncoe1  21475  cnmpt21  22822  cfilucfil  23715  ulmss  25556  fsumdvdscom  26334  dchrisumlema  26636  dchrisumlem2  26638  cnlnadjlem5  30433  rspc2daf  30816  disjabrex  30921  disjabrexf  30922  aciunf1lem  30999  fnpreimac  31008  fsumiunle  31143  nsgqusf1olem1  31598  ordtconnlem1  31874  esumiun  32062  bnj1366  32809  bnj1385  32812  bnj981  32930  bnj1228  32991  bnj1398  33014  bnj1445  33024  bnj1449  33028  bnj1463  33035  untsucf  33651  setinds  33754  tfisg  33786  frpoins3xpg  33787  nosupbnd1  33917  noinfbnd1  33932  poimirlem26  35803  poimirlem27  35804  indexdom  35892  filbcmb  35898  sdclem1  35901  scottexf  36326  scott0f  36327  cdleme31sn1  38395  cdlemk36  38927  setindtrs  40847  nfscott  41857  scottabf  41858  evth2f  42558  evthf  42570  uzwo4  42601  disjinfi  42731  choicefi  42740  rnmptbd2lem  42794  rnmptbdlem  42801  ssfiunibd  42848  infxrunb2  42907  supxrunb3  42939  supxrleubrnmpt  42946  allbutfiinf  42960  suprleubrnmpt  42962  infxrgelbrnmpt  42994  climinff  43152  limsupre3uzlem  43276  xlimmnfv  43375  xlimpnfv  43379  cncfshift  43415  cncficcgt0  43429  stoweidlem31  43572  stoweidlem34  43575  stoweidlem35  43576  stoweidlem51  43592  stoweidlem53  43594  stoweidlem54  43595  stoweidlem57  43598  stoweidlem59  43600  stoweidlem60  43601  fourierdlem31  43679  fourierdlem73  43720  iundjiun  43998  meaiuninc3v  44022  issmfle  44281  issmfgt  44292  issmfge  44305  smfpimcc  44341  smfsup  44347  smfinf  44351  2reu3  44602  2reu8i  44605  ichreuopeq  44925  reupr  44974  reuopreuprim  44978