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

Theorem ralimi 2631
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 10 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2629 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ral2imi  2632  r19.26  2688  r19.29  2696  rr19.3v  2922  rr19.28v  2923  reu3  2968  uniiunlem  3273  reupick2  3467  uniss2  3874  ss2iun  3936  iineq2  3938  iunss2  3963  disjss2  4012  disjeq2  4013  reusv2lem5  4555  reusv3i  4557  tfis  4661  issref  5072  dmmptg  5186  fununi  5332  fun11uni  5334  fnmpt  5386  fun11iun  5509  mpteqb  5630  chfnrn  5652  dffo5  5693  ffvresb  5706  fmptcof  5708  zfrep6  5764  mpt22eqb  5969  ralrnmpt2  5974  fnmpt2  6208  mpt2exxg  6211  frxp  6241  smores  6385  riiner  6748  ixpn0  6864  boxriin  6874  unifi2  7162  wemaplem2  7278  xpwdomg  7315  rankonidlem  7516  acni3  7690  dfac5  7771  dfac12lem2  7786  kmlem6  7797  kmlem8  7799  kmlem13  7804  cfsmolem  7912  fin23lem40  7993  isf32lem2  7996  fin1a2s  8056  hsmexlem2  8069  hsmex3  8076  axcc4  8081  domtriomlem  8084  dcomex  8089  ac6num  8122  iundom  8180  unirnfdomd  8205  konigthlem  8206  iunctb  8212  gch3  8318  wununi  8344  wunpw  8345  wunpr  8347  eltsk2g  8389  tskpwss  8390  tskpw  8391  grupw  8433  gruurn  8436  intgru  8452  grothpw  8464  grothpwex  8465  grothomex  8467  axgroth3  8469  suplem1pr  8692  supexpr  8694  supsr  8750  fimaxre3  9719  xrsupexmnf  10639  xrinfmexpnf  10640  rexanre  11846  rexuz3  11848  cau3lem  11854  caubnd2  11857  caubnd  11858  rlim0  11998  rlim0lt  11999  climi2  12001  climi0  12002  climrlim2  12037  rlimres  12048  o1rlimmul  12108  caurcvg  12165  caurcvg2  12166  caucvg  12167  caucvgb  12168  sumeq2  12183  ndvdssub  12622  gcdcllem1  12706  vdwnnlem1  13058  imasaddfnlem  13446  catidex  13592  catlid  13601  catrid  13602  catcocl  13603  catpropd  13628  subcidcl  13734  funcid  13760  setcepi  13936  tsrss  14348  laspwcl  14359  lanfwcl  14360  mgmidmo  14386  gsumval2  14476  issubg2  14652  gagrpid  14764  gaass  14767  dprdcntz  15259  dprddisj  15260  abveq0  15607  abvmul  15610  abvtri  15611  phllmhm  16552  ipcj  16554  ipeq0  16558  eltg2b  16713  iincld  16792  iuncld  16798  isclo2  16841  neips  16866  lmcvg  17008  t1t0  17092  hauscmplem  17149  1stcelcls  17203  ptuni2  17287  pttopon  17307  ptcld  17323  ptcnplem  17331  txtube  17350  txlm  17358  xkococnlem  17369  fbun  17551  isfil2  17567  ptcmplem4  17765  tmdcn2  17788  xmeteq0  17919  xmettri2  17921  metrest  18086  tngngp  18186  iscau4  18721  cmetcaulem  18730  caussi  18739  volfiniun  18920  iunmbl  18926  voliun  18927  mbfdm  18999  itg2seq  19113  itg2i1fseqle  19125  itg2i1fseq2  19127  iblcnlem  19159  limcresi  19251  limciun  19260  rolle  19353  ulmss  19790  rlimcnp  20276  isgrpo  20879  grpoidinv  20891  grpoideu  20892  grpoidval  20899  grpoidinv2  20901  opidon  21005  exidu1  21009  grpomndo  21029  rngoideu  21067  rngodi  21068  rngodir  21069  rngoass  21070  rngoueqz  21113  vcid  21123  vcdi  21124  vcdir  21125  vcass  21126  nvs  21244  nvz  21251  nvtri  21252  ajmoi  21453  adjmo  22428  cnlnssadj  22676  mdbr3  22893  mdbr4  22894  mdsl1i  22917  dmdbr6ati  23019  dmdbr7ati  23020  fnmptf  23242  hasheuni  23468  sigaclcu2  23496  prsiga  23507  measvunilem  23555  cntmeas  23568  cvmsdisj  23816  cvmshmeo  23817  cvmliftlem15  23844  cvmlift2lem12  23860  untangtr  24075  cprodeq2  24136  elpotr  24208  dfon2lem7  24216  dfon2lem8  24217  tfisg  24275  wfisg  24280  frinsg  24316  poseq  24324  colinearalg  24610  axpasch  24641  axeuclid  24663  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  ovoliunnfl  25001  domfldrefc  25160  ranfldrefc  25161  domintrefb  25166  celsor  25214  ab2rexexg2  25224  domintrefc  25228  mapmapmap  25251  dstr  25274  labs1  25291  labs2  25293  prodeq3  25412  fprodadd  25455  fprodsub  25482  fldax3  25533  fldax4  25534  fldax5  25535  vecax3  25558  vecax4  25559  vecax5  25560  vecax6  25561  glmrngo  25585  svli2  25587  basexre  25625  intopcoaconlem3b  25641  intopcoaconb  25643  intopcoaconc  25644  altretop  25703  imonclem  25916  iepiclem  25926  tartarmap  25991  fnckleb  26149  opnrebl2  26339  fnemeet2  26419  fnejoin1  26420  fnejoin2  26421  frinfm  26519  caushft  26580  sstotbnd3  26603  prdstotbnd  26621  heibor1lem  26636  bfplem2  26650  rngohomadd  26703  rngohommul  26704  idladdcl  26747  idllmulcl  26748  idlrmulcl  26749  ispridl2  26766  lerabdioph  26989  ltrabdioph  26992  nerabdioph  26993  dvdsrabdioph  26994  rencldnfi  27007  dford3  27224  ralbidar  27751  rexbidar  27752  stoweidlem7  27859  stoweidlem60  27912  1to3vfriendship  28432  bnj1498  29407  pmapglbx  30580  ltrnnid  30947  cdlemefrs32fva  31211
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator