MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralimdv Unicode version

Theorem ralimdv 2774
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
Hypothesis
Ref Expression
ralimdv.1
Assertion
Ref Expression
ralimdv
Distinct variable group:   ,

Proof of Theorem ralimdv
StepHypRef Expression
1 ralimdv.1 . . 3
21adantr 455 . 2
32ralimdva 2773 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1749  A.wral 2694
This theorem is referenced by:  poss  4614  sess1  4659  sess2  4660  riinint  5067  iinpreima  5803  dffo4  5829  dffo5  5830  isoini2  5998  tfindsg  6441  abianfp  6873  iiner  7133  xpf1o  7432  dffi3  7628  brwdom3  7744  xpwdomg  7747  bndrank  7995  cfub  8365  cff1  8374  cfflb  8375  cfslb2n  8384  cofsmo  8385  cfcoflem  8388  pwcfsdom  8694  fpwwe2lem13  8755  inawinalem  8802  grupr  8910  fsequb  11738  cau3lem  12783  caubnd2  12786  caubnd  12787  rlim2lt  12916  rlim3  12917  climshftlem  12993  isercolllem1  13083  climcau  13089  caucvgb  13098  serf0  13099  cvgcmp  13219  mreriincl  14476  acsfn1c  14540  islss4  16852  riinopn  18225  fiinbas  18261  baspartn  18263  isclo2  18396  lmcls  18610  lmcnp  18612  isnrm3  18667  1stcelcls  18769  llyss  18787  nllyss  18788  ptpjpre1  18848  txlly  18913  txnlly  18914  tx1stc  18927  xkococnlem  18936  fbunfip  19146  filssufilg  19188  cnpflf2  19277  fcfnei  19312  isucn2  19554  rescncf  20173  lebnum  20236  cfilss  20481  fgcfil  20482  iscau4  20490  cmetcaulem  20499  cfilres  20507  caussi  20508  ovolunlem1  20680  ulmclm  21593  ulmcaulem  21600  ulmcau  21601  ulmss  21603  rlimcnp  22100  cxploglim  22112  lgsdchr  22428  pntlemp  22600  axcontlem4  22892  nmlnoubi  23875  lnon0  23877  disjpreima  25608  resspos  25798  resstos  25799  submarchi  25882  iccllyscon  26842  cvmlift2lem1  26894  setlikess  27358  upixp  28294  caushft  28328  sstotbnd3  28346  totbndss  28347  unichnidl  28502  ispridl2  28509  elrfirn2  28704  mzpsubst  28758  eluzrabdioph  28817  ralralimp  29793  modfsummods  29918  usg2wlkeq  29963  3cyclfrgrarn2  30280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-12 1785
This theorem depends on definitions:  df-bi 179  df-an 364  df-ex 1582  df-nf 1585  df-ral 2699
  Copyright terms: Public domain W3C validator