Theorem nfral 2945

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	|- F/_ x A
nfral.2	|- F/ x ph

Assertion

Ref	Expression
nfral	|- F/ x A. y e. A ph

Proof of Theorem nfral

Step	Hyp	Ref	Expression
1		nftru 1730	. . 3 |- F/ y T.
2		nfral.1	. . . 4 |- F/_ x A
3	2	a1i 11	. . 3 |- ( T. -> F/_ x A )
4		nfral.2	. . . 4 |- F/ x ph
5	4	a1i 11	. . 3 |- ( T. -> F/ x ph )
6	1, 3, 5	nfrald 2944	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	trud 1493	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1484   F/wnf 1708   F/_wnfc 2751   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  nfra2  2946  rspc2  3320  sbcralt  3510  reu8nf  3516  raaan  4082  nfint  4486  nfiin  4549  disjxun  4651  nfpo  5040  nfso  5041  nffr  5088  nfse  5089  ralxpf  5268  wfisg  5715  dff13f  6513  nfiso  6572  mpt2eq123  6714  fun11iun  7126  fmpt2x  7236  ovmptss  7258  nfwrecs  7409  xpf1o  8122  ac6sfi  8204  nfoi  8419  scottexs  8750  scott0s  8751  lble  10975  nnwof  11754  fzrevral  12425  reuccats1  13480  rlimcld2  14309  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  gsummoncoe1  19674  cnmpt21  21474  cfilucfil  22364  ulmss  24151  fsumdvdscom  24911  dchrisumlema  25177  dchrisumlem2  25179  rspc2vd  27129  cnlnadjlem5  28930  disjabrex  29395  disjabrexf  29396  aciunf1lem  29462  fsumiunle  29575  ordtconnlem1  29970  esumiun  30156  bnj1366  30900  bnj1385  30903  bnj981  31020  bnj1228  31079  bnj1398  31102  bnj1445  31112  bnj1449  31116  bnj1463  31123  untsucf  31587  setinds  31683  tfisg  31716  frinsg  31742  nosupbnd1  31860  poimirlem26  33435  poimirlem27  33436  indexdom  33529  filbcmb  33535  sdclem1  33539  scottexf  33976  scott0f  33977  cdleme31sn1  35669  cdlemk36  36201  setindtrs  37592  evth2f  39174  evthf  39186  uzwo4  39221  eliuniincex  39292  disjinfi  39380  choicefi  39392  rnmptbd2lem  39463  rnmptbdlem  39470  ssfiunibd  39523  infxrunb2  39584  supxrunb3  39623  supxrleubrnmpt  39632  allbutfiinf  39647  suprleubrnmpt  39649  infxrgelbrnmpt  39683  climinff  39843  limsupre3uzlem  39967  xlimmnfv  40060  xlimpnfv  40064  cncfshift  40087  cncficcgt0  40101  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem51  40268  stoweidlem53  40270  stoweidlem54  40271  stoweidlem57  40274  stoweidlem59  40276  stoweidlem60  40277  fourierdlem31  40355  fourierdlem73  40396  iundjiun  40677  issmfle  40954  issmfgt  40965  issmfge  40978  smfpimcc  41014  smfsup  41020  smfinf  41024  cbvral2  41172  raaan2  41175  2reu3  41188