Theorem nfral 2929

Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)

Hypotheses

Ref	Expression
nfral.1	⊢ Ⅎ𝑥𝐴
nfral.2	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfral	⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Proof of Theorem nfral

Step	Hyp	Ref	Expression
1		nftru 1721	. . 3 ⊢ Ⅎ𝑦⊤
2		nfral.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfral.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrald 2928	. 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	trud 1484	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1476  Ⅎwnf 1699  Ⅎwnfc 2738  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901

This theorem is referenced by:  nfra2  2930  rspc2  3292  sbcralt  3477  raaan  4032  nfint  4421  nfiin  4485  disjxun  4581  nfpo  4964  nfso  4965  nffr  5012  nfse  5013  ralxpf  5190  wfisg  5632  dff13f  6417  nfiso  6472  mpt2eq123  6612  fun11iun  7019  fmpt2x  7125  ovmptss  7145  nfwrecs  7296  xpf1o  8007  ac6sfi  8089  nfoi  8302  scottexs  8633  scott0s  8634  lble  10854  nnwof  11630  fzrevral  12294  rlimcld2  14157  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  gsummoncoe1  19495  cnmpt21  21284  cfilucfil  22174  ulmss  23955  fsumdvdscom  24711  dchrisumlema  24977  dchrisumlem2  24979  cnlnadjlem5  28314  disjabrex  28777  disjabrexf  28778  aciunf1lem  28844  ordtconlem1  29298  esumiun  29483  bnj1366  30154  bnj1385  30157  bnj981  30274  bnj1228  30333  bnj1398  30356  bnj1445  30366  bnj1449  30370  bnj1463  30377  untsucf  30841  setinds  30927  tfisg  30960  frinsg  30986  poimirlem26  32605  poimirlem27  32606  indexdom  32699  filbcmb  32705  sdclem1  32709  scottexf  33146  scott0f  33147  cdleme31sn1  34687  cdlemk36  35219  setindtrs  36610  evth2f  38197  evthf  38209  uzwo4  38246  eliuniincex  38323  disjinfi  38375  choicefi  38387  ssfiunibd  38464  infxrunb2  38525  climinff  38678  cncfshift  38759  cncficcgt0  38774  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem51  38944  stoweidlem53  38946  stoweidlem54  38947  stoweidlem57  38950  stoweidlem59  38952  stoweidlem60  38953  fourierdlem31  39031  fourierdlem73  39072  iundjiun  39353  issmfle  39632  issmfgt  39643  issmfge  39656  cbvral2  39821  raaan2  39824  2reu3  39837  rspc2vd  41437