Theorem nfralw 3313

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

This proof depends on syntax axioms:  Ⅎwnf 1816  Ⅎwnfc 2911  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2839  df-nfc 2913  df-ral 3081

This theorem is used by:  rspc2  3588  sbcralt  3823  reu8nf  3828  rspc2vd  3899  raaan  4477  raaan2  4481  reusngf  4635  rexreusng  4640  reuprg0  4663  nfint  4920  nfiin  4986  disjxun  5104  nfpo  5569  nfso  5570  nffr  5628  nfse  5629  ralxpf  5829  reuop  6311  frpoinsg  6361  dff13f  7279  nfiso  7350  mpoeq123  7512  nfofr  7721  tfisg  7886  fiun  7976  f1iun  7977  fmpox  8100  ovmptssOLD  8127  frpoins3xpg  8181  nffrecs  8326  xpf1o  9183  ac6sfi  9300  nfoi  9532  setinds  9774  frinsg  9779  nfscott  9956  scottabf  9963  scottexsOLD  9967  scott0bsOLD  9969  lble  12293  nnwof  13065  fzrevral  13770  reuccatpfxs1  14921  rlimcld2  15771  fsum2dlem  15962  fsumcom2  15966  fprod2dlem  16173  fprodcom2  16177  gsummoncoe1  22653  cnmpt21  24017  cfilucfil  24905  ulmss  26751  fsumdvdscom  27539  dchrisumlema  27842  dchrisumlem2  27844  nosupbnd1  28098  noinfbnd1  28113  cnlnadjlem5  32700  rspc2daf  33132  disjabrex  33245  disjabrexf  33246  aciunf1lem  33325  fnpreimac  33333  fsumiunle  33487  nsgqusf1olem1  34031  ordtconnlem1  34623  esumiun  34793  bnj1366  35526  bnj1385  35529  bnj981  35647  bnj1228  35708  bnj1398  35731  bnj1445  35741  bnj1449  35745  bnj1463  35752  srepdf  36086  untsucf  36652  poimirlem26  38755  poimirlem27  38756  indexdom  38859  filbcmb  38865  sdclem1  38868  scottexf  39291  scott0f  39292  cdleme31sn1  41629  cdlemk36  42161  setindtrs  44223  oaun3lem1  44566  nfrelp  46132  modelaxrep  46164  evth2f  46235  evthf  46247  uzwo4  46273  disjinfi  46410  choicefi  46417  rnmptbd2lem  46463  rnmptbdlem  46470  ssfiunibd  46528  infxrunb2  46582  supxrunb3  46613  supxrleubrnmpt  46619  allbutfiinf  46633  suprleubrnmpt  46635  infxrgelbrnmpt  46667  caucvgbf  46702  climinff  46826  limsupre3uzlem  46948  xlimmnfv  47047  xlimpnfv  47051  cncfshift  47087  cncficcgt0  47101  stoweidlem31  47244  stoweidlem34  47247  stoweidlem35  47248  stoweidlem51  47264  stoweidlem53  47266  stoweidlem54  47267  stoweidlem57  47270  stoweidlem59  47272  stoweidlem60  47273  fourierdlem31  47351  fourierdlem73  47392  iundjiun  47673  meaiuninc3v  47697  issmfle  47958  issmfgt  47969  issmfge  47983  smfpimcc  48021  smfsup  48027  smfinf  48031  2reu3  48384  2reu8i  48387  ichreuopeq  48758  reupr  48807  reuopreuprim  48811  nfrals  51178  nfralseu  51209