Theorem nfralw 3309

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

This proof depends on syntax axioms:  Ⅎwnf 1815  Ⅎwnfc 2907  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-10 2177  ax-11 2193  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-clel 2835  df-nfc 2909  df-ral 3077

This theorem is used by:  rspc2  3584  sbcralt  3818  reu8nf  3823  rspc2vd  3894  raaan  4473  raaan2  4477  reusngf  4634  rexreusng  4639  reuprg0  4662  nfint  4916  nfiin  4982  disjxun  5100  nfpo  5564  nfso  5565  nffr  5623  nfse  5624  ralxpf  5823  reuop  6296  frpoinsg  6346  dff13f  7259  nfiso  7330  mpoeq123  7492  nfofr  7700  tfisg  7865  fiun  7955  f1iun  7956  fmpox  8078  ovmptss  8104  frpoins3xpg  8157  nffrecs  8301  xpf1o  9158  ac6sfi  9275  nfoi  9508  setinds  9750  frinsg  9755  nfscott  9932  scottabf  9939  scottexsOLD  9943  scott0bsOLD  9945  lble  12269  nnwof  13041  fzrevral  13746  reuccatpfxs1  14896  rlimcld2  15745  fsum2dlem  15936  fsumcom2  15940  fprod2dlem  16147  fprodcom2  16151  gsummoncoe1  22626  cnmpt21  23990  cfilucfil  24878  ulmss  26724  fsumdvdscom  27512  dchrisumlema  27815  dchrisumlem2  27817  nosupbnd1  28071  noinfbnd1  28086  cnlnadjlem5  32673  rspc2daf  33063  disjabrex  33176  disjabrexf  33177  aciunf1lem  33256  fnpreimac  33264  fsumiunle  33420  nsgqusf1olem1  33964  ordtconnlem1  34556  esumiun  34726  bnj1366  35459  bnj1385  35462  bnj981  35580  bnj1228  35641  bnj1398  35664  bnj1445  35674  bnj1449  35678  bnj1463  35685  untsucf  36475  poimirlem26  38565  poimirlem27  38566  indexdom  38669  filbcmb  38675  sdclem1  38678  scottexf  39101  scott0f  39102  cdleme31sn1  41439  cdlemk36  41971  setindtrs  44032  oaun3lem1  44376  nfrelp  45939  modelaxrep  45971  evth2f  46032  evthf  46044  uzwo4  46070  disjinfi  46207  choicefi  46214  rnmptbd2lem  46260  rnmptbdlem  46267  ssfiunibd  46325  infxrunb2  46379  supxrunb3  46410  supxrleubrnmpt  46416  allbutfiinf  46430  suprleubrnmpt  46432  infxrgelbrnmpt  46464  caucvgbf  46499  climinff  46623  limsupre3uzlem  46745  xlimmnfv  46844  xlimpnfv  46848  cncfshift  46884  cncficcgt0  46898  stoweidlem31  47041  stoweidlem34  47044  stoweidlem35  47045  stoweidlem51  47061  stoweidlem53  47063  stoweidlem54  47064  stoweidlem57  47067  stoweidlem59  47069  stoweidlem60  47070  fourierdlem31  47148  fourierdlem73  47189  iundjiun  47470  meaiuninc3v  47494  issmfle  47755  issmfgt  47766  issmfge  47780  smfpimcc  47818  smfsup  47824  smfinf  47828  2reu3  48180  2reu8i  48183  ichreuopeq  48555  reupr  48604  reuopreuprim  48608  nfrals  50900  nfralseu  50931