Theorem ralimdv 2867

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1632). (Contributed by NM, 8-Oct-2003.)

Hypothesis

Ref	Expression
ralimdv.1

Assertion

Ref	Expression
ralimdv

Distinct variable group:   ,

Proof of Theorem ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3
2	1	adantr 465	. 2
3	2	ralimdva 2865	1

Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807

This theorem is referenced by:  poss  4807  sess1  4852  sess2  4853  riinint  5264  iinpreima  6017  dffo4  6047  dffo5  6048  isoini2  6235  tfindsg  6695  iiner  7402  xpf1o  7699  dffi3  7911  brwdom3  8029  xpwdomg  8032  bndrank  8280  cfub  8650  cff1  8659  cfflb  8660  cfslb2n  8669  cofsmo  8670  cfcoflem  8673  pwcfsdom  8979  fpwwe2lem13  9041  inawinalem  9088  grupr  9196  fsequb  12085  cau3lem  13187  caubnd2  13190  caubnd  13191  rlim2lt  13320  rlim3  13321  climshftlem  13397  isercolllem1  13487  climcau  13493  caucvgb  13502  serf0  13503  modfsummods  13607  cvgcmp  13630  mreriincl  14995  acsfn1c  15059  islss4  17608  riinopn  19417  fiinbas  19453  baspartn  19455  isclo2  19589  lmcls  19803  lmcnp  19805  isnrm3  19860  1stcelcls  19962  llyss  19980  nllyss  19981  ptpjpre1  20072  txlly  20137  txnlly  20138  tx1stc  20151  xkococnlem  20160  fbunfip  20370  filssufilg  20412  cnpflf2  20501  fcfnei  20536  isucn2  20782  rescncf  21401  lebnum  21464  cfilss  21709  fgcfil  21710  iscau4  21718  cmetcaulem  21727  cfilres  21735  caussi  21736  ovolunlem1  21908  ulmclm  22782  ulmcaulem  22789  ulmcau  22790  ulmss  22792  rlimcnp  23295  cxploglim  23307  lgsdchr  23623  pntlemp  23795  axcontlem4  24270  usg2wlkeq  24708  3cyclfrgrarn2  25014  nmlnoubi  25711  lnon0  25713  disjpreima  27445  resspos  27647  resstos  27648  submarchi  27730  crefss  27852  iccllyscon  28695  cvmlift2lem1  28747  ss2mcls  28928  mclsax  28929  setlikess  29275  upixp  30220  caushft  30254  sstotbnd3  30272  totbndss  30273  unichnidl  30428  ispridl2  30435  elrfirn2  30628  mzpsubst  30681  eluzrabdioph  30739  fourierdlem103  31992  fourierdlem104  31993  ralralimp  32295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812