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

Theorem ralimi 2850
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1
Assertion
Ref Expression
ralimi

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3
21a1i 11 . 2
32ralimia 2848 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ral2imiOLD  2852  r19.26  2984  r19.29  2992  rr19.3v  3241  rr19.28v  3242  reu3  3289  uniiunlem  3587  reupick2  3783  uniss2  4282  ss2iun  4346  iineq2  4348  iunss2  4375  disjss2  4425  disjeq2  4426  reusv2lem5  4657  reusv3i  4659  ssrel2  5098  issref  5385  dmmptg  5509  fununi  5659  fnmpt  5712  mpteqb  5970  chfnrn  5998  fvn0ssdmfun  6022  dffo5  6048  ffvresb  6062  fmptcof  6065  mpt22eqb  6411  ralrnmpt2  6417  tfis  6689  fun11uni  6754  fun11iun  6760  zfrep6  6768  fnmpt2  6868  mpt2exxg  6874  frxp  6910  smores  7042  riiner  7403  ixpn0  7521  boxriin  7531  unifi2  7830  wemaplem2  7993  xpwdomg  8032  rankonidlem  8267  acni3  8449  dfac5  8530  dfac12lem2  8545  kmlem6  8556  kmlem8  8558  kmlem13  8563  cfsmolem  8671  fin23lem40  8752  isf32lem2  8755  fin1a2s  8815  hsmexlem2  8828  hsmex3  8835  axcc4  8840  domtriomlem  8843  dcomex  8848  ac6num  8880  iundom  8938  unirnfdomd  8963  konigthlem  8964  iunctb  8970  gch3  9075  wununi  9105  wunpw  9106  wunpr  9108  eltsk2g  9150  tskpwss  9151  tskpw  9152  grupw  9194  gruurn  9197  intgru  9213  grothpw  9225  grothpwex  9226  grothomex  9228  axgroth3  9230  suplem1pr  9451  supexpr  9453  supsr  9510  fimaxre3  10517  xrsupexmnf  11525  xrinfmexpnf  11526  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  fsuppmapnn0fiubex  12098  mptnn0fsuppd  12104  rexanre  13179  rexuz3  13181  cau3lem  13187  caubnd2  13190  caubnd  13191  rlim0  13331  rlim0lt  13332  climi2  13334  climi0  13335  climrlim2  13370  rlimres  13381  o1rlimmul  13441  caurcvg  13499  caurcvg2  13500  caucvg  13501  caucvgb  13502  sumeq2  13516  prodeq2  13721  ndvdssub  14065  gcdcllem1  14149  vdwnnlem1  14513  imasaddfnlem  14925  catidex  15071  catlid  15080  catrid  15081  catcocl  15082  catpropd  15104  subcidcl  15213  funcid  15239  setcepi  15415  tsrss  15853  mgmidmo  15886  gsumval2  15907  isnmnd  15924  issubg2  16216  gagrpid  16332  gaass  16335  dprdcntz  17041  dprddisj  17042  abveq0  17475  abvmul  17478  abvtri  17479  psgndiflemB  18636  phllmhm  18667  ipcj  18669  ipeq0  18673  mdetmul  19125  pmatcollpw2lem  19278  eltg2b  19460  iincld  19540  iuncld  19546  isclo2  19589  neips  19614  neipeltop  19630  lmcvg  19763  t1t0  19849  hauscmplem  19906  bwth  19910  1stcelcls  19962  ptuni2  20077  pttopon  20097  ptcld  20114  ptcnplem  20122  txtube  20141  txlm  20149  xkococnlem  20160  fbun  20341  isfil2  20357  ptcmplem4  20555  tmdcn2  20588  ustssel  20708  isucn2  20782  ucncn  20788  xmeteq0  20841  xmettri2  20843  metrest  21027  tngngp  21168  iscau4  21718  cmetcaulem  21727  caussi  21736  volfiniun  21957  iunmbl  21963  voliun  21964  mbfdm  22035  itg2seq  22149  itg2i1fseqle  22161  itg2i1fseq2  22163  iblcnlem  22195  limcresi  22289  limciun  22298  rolle  22391  ulmss  22792  rlimcnp  23295  midf  24142  colinearalg  24213  axpasch  24244  axeuclid  24266  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  nbgraf1olem1  24441  usgfiregdegfi  24911  1to3vfriendship  25008  frconngra  25021  frgraregorufr0  25052  usgreghash2spot  25069  isgrpo  25198  grpoidinv  25210  grpoideu  25211  grpoidval  25218  grpoidinv2  25220  opidonOLD  25324  exidu1  25328  grpomndo  25348  rngoideu  25386  rngodi  25387  rngodir  25388  rngoass  25389  rngoueqz  25432  vcid  25444  vcdi  25445  vcdir  25446  vcass  25447  nvs  25565  nvz  25572  nvtri  25573  ajmoi  25774  adjmo  26751  cnlnssadj  26999  mdbr3  27216  mdbr4  27217  mdsl1i  27240  dmdbr6ati  27342  dmdbr7ati  27343  disjunsn  27453  fnmptf  27500  xrge0infss  27580  hasheuni  28091  sigaclcu2  28120  prsiga  28131  measvunilem  28183  cntmeas  28197  signsply0  28508  cvmsdisj  28715  cvmshmeo  28716  cvmliftlem15  28743  cvmlift2lem12  28759  untangtr  29086  elpotr  29213  dfon2lem7  29221  dfon2lem8  29222  tfisg  29284  wfisg  29289  frinsg  29325  poseq  29333  heicant  30049  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  opnrebl2  30139  fnemeet2  30185  fnejoin1  30186  fnejoin2  30187  frinfm  30226  caushft  30254  sstotbnd3  30272  prdstotbnd  30290  heibor1lem  30305  bfplem2  30319  rngohomadd  30372  rngohommul  30373  idladdcl  30416  idllmulcl  30417  idlrmulcl  30418  ispridl2  30435  mpt2bi123f  30571  iineq12f  30573  mptbi12f  30575  lerabdioph  30738  ltrabdioph  30741  nerabdioph  30742  dvdsrabdioph  30743  rencldnfi  30755  dford3  30970  ralbidar  31354  rexbidar  31355  stoweidlem60  31842  mpt2exxg2  32927  bnj1498  34117  pmapglbx  35493  ltrnnid  35860  cdlemefrs32fva  36126  pwelg  37745  pwinfi2  37747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator