Theorem ralimdva 2865

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
ralimdva.1

Assertion

Ref	Expression
ralimdva

Distinct variable group:   ,

Proof of Theorem ralimdva

Step	Hyp	Ref	Expression
1		ralimdva.1	. . . 4
2	1	ex 434	. . 3
3	2	a2d 26	. 2
4	3	ralimdv2 2864	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807

This theorem is referenced by:  ralimdv  2867  ralimdvva  2868  wereu2  4881  fveqressseq  6027  f1mpt  6169  isores3  6231  caofrss  6573  caoftrn  6575  sorpssuni  6589  sorpssint  6590  onint  6630  smogt  7057  fisupg  7788  ixpfi2  7838  fissuni  7845  indexfi  7848  wemaplem2  7993  rankonidlem  8267  ac5num  8438  acni2  8448  acndom2  8456  alephle  8490  dfac5  8530  cfsmolem  8671  isf34lem7  8780  isf34lem6  8781  fin1a2s  8815  acncc  8841  ttukeylem6  8915  fpwwe2lem8  9036  gchina  9098  inar1  9174  tskord  9179  grudomon  9216  grur1a  9218  dedekind  9765  fimaxre  10515  uzwo  11173  uzwoOLD  11174  xrsupsslem  11527  xrinfmsslem  11528  fsuppmapnn0fiub0  12099  rexanre  13179  rexuz3  13181  rexico  13186  cau3lem  13187  limsupval2  13303  rlim2lt  13320  rlim3  13321  lo1bdd2  13347  lo1bddrp  13348  o1lo1  13360  climrlim2  13370  2clim  13395  o1co  13409  rlimcn1  13411  rlimcn2  13413  climcn1  13414  climcn2  13415  subcn2  13417  o1of2  13435  rlimo1  13439  o1rlimmul  13441  lo1add  13449  lo1mul  13450  climsqz  13463  climsqz2  13464  rlimsqzlem  13471  lo1le  13474  climbdd  13494  caucvgrlem  13495  caucvgrlem2  13497  caurcvg2  13500  iseralt  13507  cvgcmp  13630  cvgcmpce  13632  gcdcllem1  14149  pcfac  14418  pockthg  14424  infpnlem1  14428  prmreclem2  14435  prmreclem3  14436  vdwlem11  14509  vdwlem13  14511  vdwnnlem3  14515  isacs2  15050  acsfn1  15058  acsfn2  15060  catpropd  15104  drsdirfi  15567  ipodrsima  15795  isacs5  15802  mrelatglb  15814  mrelatlub  15816  isgrpinv  16100  issubg4  16220  gsmsymgreqlem2  16456  gexdvds  16604  gexcl3  16607  sylow2blem3  16642  cyggeninv  16886  gsummptnn0fz  17014  dprdff  17046  dprdffOLD  17052  issubdrg  17454  mptcoe1fsupp  18255  cply1coe0bi  18342  gsummoncoe1  18346  cygznlem3  18608  scmatdmat  19017  mdetdiagid  19102  mdetunilem9  19122  cpmatmcllem  19219  m2cpminvid2lem  19255  decpmatmulsumfsupp  19274  pmatcollpw1lem1  19275  pmatcollpw2lem  19278  pmatcollpwfi  19283  pm2mpf1  19300  mptcoe1matfsupp  19303  mp2pm2mplem4  19310  pm2mpmhmlem1  19319  pm2mp  19326  chpdmat  19342  chpscmat  19343  cpmidpmatlem3  19373  cayhamlem4  19389  neiptopnei  19633  cncnp  19781  isnrm2  19859  isreg2  19878  2ndcdisj  19957  islly2  19985  dislly  19998  kgen2ss  20056  ptbasfi  20082  ptclsg  20116  prdstopn  20129  txtube  20141  txlm  20149  isr0  20238  filuni  20386  alexsubALTlem3  20549  ptcmplem3  20554  ptcmplem4  20555  tsmsxplem1  20655  prdsmet  20873  metequiv2  21013  metcnpi3  21049  nmoleub  21238  rescncf  21401  cncfco  21411  evth  21459  lebnumlem3  21463  xlebnum  21465  nmoleub2lem2  21599  nmhmcn  21603  lmmcvg  21700  cmetcaulem  21727  caubl  21746  bcth3  21770  ovollb2lem  21899  ovoliunlem2  21914  ovolicc2lem3  21930  ovolicc2lem4  21931  nulmbl2  21947  volsup  21966  ioombl1lem4  21971  dyadmax  22007  vitalilem2  22018  vitalilem5  22021  mbfi1flimlem  22129  itg2seq  22149  itg2addlem  22165  itgcn  22249  limciun  22298  rolle  22391  dvfsumrlim  22432  itgsubst  22450  aannenlem1  22724  aalioulem3  22730  ulmcaulem  22789  ulmcau  22790  ulmss  22792  ulmbdd  22793  ulmcn  22794  ulmdvlem3  22797  mtest  22799  iblulm  22802  itgulm  22803  rlimcnp  23295  xrlimcnp  23298  rlimcxp  23303  o1cxp  23304  amgm  23320  ftalem2  23347  isppw2  23389  mumullem2  23454  2sqlem6  23644  chtppilimlem2  23659  chtppilim  23660  pntrsumbnd2  23752  pntlem3  23794  isperp2  24092  axeuclidlem  24265  axeuclid  24266  cusgrares  24472  edgwlk  24531  usgrnloop  24565  redwlk  24608  cusconngra  24676  wlkiswwlk1  24690  wlkiswwlk2lem4  24694  usg2wlkeq  24708  wwlknred  24723  wwlkm1edg  24735  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  usgravd00  24919  cusgraisrusgra  24938  rusgraprop2  24942  rusgraprop3  24943  frisusgranb  24997  2pthfrgrarn  25009  2pthfrgrarn2  25010  2pthfrgra  25011  3cyclfrgra  25015  frgrancvvdeq  25042  frgrancvvdgeq  25043  nmoub3i  25688  ubthlem1  25786  ubthlem3  25788  ocsh  26201  chintcli  26249  chscllem2  26556  nmopub2tALT  26828  nmfnleub2  26845  lnconi  26952  riesz1  26984  rnbra  27026  leopadd  27051  leopmuli  27052  leoptr  27056  dmdbr3  27224  dmdbr4  27225  dmdbr5  27227  mdsl0  27229  mdsymlem6  27327  cdj1i  27352  xrge0infss  27580  cmppcmp  27861  lmxrge0  27934  lgambdd  28579  cvmlift2lem12  28759  finixpnum  30038  heicant  30049  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  opnrebl2  30139  neibastop1  30177  neibastop2lem  30178  neibastop3  30180  filbcmb  30231  nninfnub  30244  geomcau  30252  sstotbnd2  30270  isbndx  30278  prdsbnd  30289  heibor1lem  30305  heiborlem1  30307  heibor  30317  rrncmslem  30328  intidl  30426  elrfirn2  30628  isnacs3  30642  rencldnfilem  30754  kelac1  31009  acsfn1p  31148  cvgdvgrat  31194  neglimc  31653  stoweidlem7  31789  fourierdlem73  31962  copisnmnd  32497  2zrngnmlid2  32757  ply1mulgsumlem1  32986  ply1mulgsumlem3  32988  ply1mulgsumlem4  32989  snlindsntor  33072  pclclN  35615  lauteq  35819  ltrnid  35859  mapdh9a  37517

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