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

Theorem ralimi 2783
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ralimi  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2781 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   A.wral 2707
This theorem is referenced by:  ral2imi  2784  r19.26  2840  r19.29  2848  rr19.3v  3079  rr19.28v  3080  reu3  3126  uniiunlem  3433  reupick2  3629  uniss2  4048  ss2iun  4110  iineq2  4112  iunss2  4138  disjss2  4188  disjeq2  4189  reusv2lem5  4731  reusv3i  4733  tfis  4837  ssrel2  4969  issref  5250  dmmptg  5370  fununi  5520  fun11uni  5522  fnmpt  5574  fun11iun  5698  mpteqb  5822  chfnrn  5844  dffo5  5889  ffvresb  5903  fmptcof  5905  zfrep6  5971  mpt22eqb  6182  ralrnmpt2  6187  fnmpt2  6422  mpt2exxg  6425  frxp  6459  smores  6617  riiner  6980  ixpn0  7097  boxriin  7107  unifi2  7399  wemaplem2  7519  xpwdomg  7556  rankonidlem  7757  acni3  7933  dfac5  8014  dfac12lem2  8029  kmlem6  8040  kmlem8  8042  kmlem13  8047  cfsmolem  8155  fin23lem40  8236  isf32lem2  8239  fin1a2s  8299  hsmexlem2  8312  hsmex3  8319  axcc4  8324  domtriomlem  8327  dcomex  8332  ac6num  8364  iundom  8422  unirnfdomd  8447  konigthlem  8448  iunctb  8454  gch3  8556  wununi  8586  wunpw  8587  wunpr  8589  eltsk2g  8631  tskpwss  8632  tskpw  8633  grupw  8675  gruurn  8678  intgru  8694  grothpw  8706  grothpwex  8707  grothomex  8709  axgroth3  8711  suplem1pr  8934  supexpr  8936  supsr  8992  fimaxre3  9962  xrsupexmnf  10888  xrinfmexpnf  10889  rexanre  12155  rexuz3  12157  cau3lem  12163  caubnd2  12166  caubnd  12167  rlim0  12307  rlim0lt  12308  climi2  12310  climi0  12311  climrlim2  12346  rlimres  12357  o1rlimmul  12417  caurcvg  12475  caurcvg2  12476  caucvg  12477  caucvgb  12478  sumeq2  12493  ndvdssub  12932  gcdcllem1  13016  vdwnnlem1  13368  imasaddfnlem  13758  catidex  13904  catlid  13913  catrid  13914  catcocl  13915  catpropd  13940  subcidcl  14046  funcid  14072  setcepi  14248  tsrss  14660  laspwcl  14671  lanfwcl  14672  mgmidmo  14698  gsumval2  14788  issubg2  14964  gagrpid  15076  gaass  15079  dprdcntz  15571  dprddisj  15572  abveq0  15919  abvmul  15922  abvtri  15923  phllmhm  16868  ipcj  16870  ipeq0  16874  eltg2b  17029  iincld  17108  iuncld  17114  isclo2  17157  neips  17182  neipeltop  17198  lmcvg  17331  t1t0  17417  hauscmplem  17474  1stcelcls  17529  ptuni2  17613  pttopon  17633  ptcld  17650  ptcnplem  17658  txtube  17677  txlm  17685  xkococnlem  17696  fbun  17877  isfil2  17893  ptcmplem4  18091  tmdcn2  18124  ustssel  18240  isucn2  18314  ucncn  18320  xmeteq0  18373  xmettri2  18375  metrest  18559  tngngp  18700  iscau4  19237  cmetcaulem  19246  caussi  19255  volfiniun  19446  iunmbl  19452  voliun  19453  mbfdm  19523  itg2seq  19637  itg2i1fseqle  19649  itg2i1fseq2  19651  iblcnlem  19683  limcresi  19777  limciun  19786  rolle  19879  ulmss  20318  rlimcnp  20809  nbgraf1olem1  21456  isgrpo  21789  grpoidinv  21801  grpoideu  21802  grpoidval  21809  grpoidinv2  21811  opidon  21915  exidu1  21919  grpomndo  21939  rngoideu  21977  rngodi  21978  rngodir  21979  rngoass  21980  rngoueqz  22023  vcid  22035  vcdi  22036  vcdir  22037  vcass  22038  nvs  22156  nvz  22163  nvtri  22164  ajmoi  22365  adjmo  23340  cnlnssadj  23588  mdbr3  23805  mdbr4  23806  mdsl1i  23829  dmdbr6ati  23931  dmdbr7ati  23932  fnmptf  24079  hasheuni  24480  sigaclcu2  24508  prsiga  24519  measvunilem  24571  cntmeas  24585  cvmsdisj  24962  cvmshmeo  24963  cvmliftlem15  24990  cvmlift2lem12  25006  untangtr  25168  prodeq2  25245  elpotr  25413  dfon2lem7  25421  dfon2lem8  25422  tfisg  25484  wfisg  25489  frinsg  25525  poseq  25533  colinearalg  25854  axpasch  25885  axeuclid  25907  axcontlem2  25909  axcontlem4  25911  axcontlem7  25914  axcontlem8  25915  ovoliunnfl  26259  voliunnfl  26261  volsupnfl  26262  opnrebl2  26337  fnemeet2  26409  fnejoin1  26410  fnejoin2  26411  frinfm  26450  caushft  26480  sstotbnd3  26498  prdstotbnd  26516  heibor1lem  26531  bfplem2  26545  rngohomadd  26598  rngohommul  26599  idladdcl  26642  idllmulcl  26643  idlrmulcl  26644  ispridl2  26661  lerabdioph  26878  ltrabdioph  26881  nerabdioph  26882  dvdsrabdioph  26883  rencldnfi  26895  dford3  27112  ralbidar  27637  rexbidar  27638  stoweidlem60  27798  usgfiregdegfi  28425  1to3vfriendship  28471  frconngra  28484  frgraregorufr0  28514  usgreghash2spot  28531  bnj1498  29503  pmapglbx  30639  ltrnnid  31006  cdlemefrs32fva  31270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ral 2712
  Copyright terms: Public domain W3C validator