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

Theorem eqsstrd 3504
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
eqsstrd.1  |-  ( ph  ->  A  =  B )
eqsstrd.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
eqsstrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem eqsstrd
StepHypRef Expression
1 eqsstrd.2 . 2  |-  ( ph  ->  B  C_  C )
2 eqsstrd.1 . . 3  |-  ( ph  ->  A  =  B )
32sseq1d 3497 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 235 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  eqsstr3d  3505  syl6eqss  3520  fpr2g  6140  tfisi  6699  suppssof1  6959  suppss2  6960  onfununi  7068  oawordeulem  7263  oeeui  7311  nnawordex  7346  oaabslem  7352  oaabs2  7354  omabslem  7355  omabs  7356  pw2f1olem  7682  fodomr  7729  fival  7932  dffi3  7951  ordtypelem7  8039  ordtypelem8  8040  wemapso2lem  8067  cantnflt2  8177  cantnflem1  8193  tcss  8227  tcel  8228  r1val1  8256  rankuni2b  8323  tcrank  8354  cardonle  8390  harval2  8430  carduniima  8525  ackbij2  8671  cfub  8677  cflecard  8681  cfflb  8687  isf32lem8  8788  itunitc1  8848  ttukeylem7  8943  fpwwe2lem9  9062  wuncss  9169  wuncval2  9171  grur1a  9243  trclfvub  13050  cotrtrclfv  13055  relexpfld  13091  rtrclreclem4  13103  limsupgre  13520  limsupgreOLD  13521  isercolllem3  13708  4sqlem19  14876  vdwlem1  14894  vdwlem12  14905  ramub1lem1  14947  ressress  15149  imasaddfnlem  15385  imasaddflem  15387  imasvscafn  15394  imasvscaf  15396  imasless  15397  isohom  15632  ressffth  15794  acsfiindd  16374  acsmap2d  16376  dirref  16432  mrcmndind  16564  f1omvdco2  17040  pmtrfrn  17050  symgsssg  17059  symggen  17062  psgnunilem1  17085  sylow2alem2  17205  lsmssv  17230  lsmidm  17249  gsumzres  17478  dprdlub  17594  dprdf1  17601  dprdsn  17604  dprdcntz2  17606  dprd2dlem1  17609  dprd2da  17610  dmdprdsplit2lem  17613  ablfac1eu  17641  drnglpir  18412  issubassa2  18504  evlslem4  18666  evlseu  18674  znleval  19056  evpmss  19085  frlmsplit2  19262  f1lindf  19311  lpsscls  20088  tgrest  20106  resttopon  20108  rest0  20116  restfpw  20126  ordtrest  20149  ordtrest2  20151  lmcnp  20251  tgcmp  20347  uncmp  20349  hauscmplem  20352  1stcfb  20391  2ndcdisj  20402  dissnref  20474  kgencmp  20491  xkouni  20545  prdstopn  20574  txtube  20586  txcmplem2  20588  xkoptsub  20600  xkopt  20601  xkococnlem  20605  qtoprest  20663  imastopn  20666  kqdisj  20678  reghmph  20739  nrmhmph  20740  fbssfi  20783  trfilss  20835  trfg  20837  elfm3  20896  alexsubALTlem3  20995  alexsubALT  20997  cnextf  21012  cnextcn  21013  clsnsg  21055  tgpconcompeqg  21057  qustgphaus  21068  trust  21175  ustuqtop3  21189  neipcfilu  21242  metequiv2  21456  prdsxmslem2  21475  metustfbas  21503  icccmplem1  21751  metdstri  21779  pi1addf  21971  pi1addval  21972  caubl  22170  caublcls  22171  relcmpcmet  22179  minveclem4  22267  hlhil  22278  ovolficcss  22301  uniioombllem3a  22419  uniioombllem3  22420  dyadss  22429  opnmbllem  22436  i1fima2  22514  limcfval  22704  dvfval  22729  dvnres  22762  dvivth  22839  lhop  22845  taylf  23181  xrlimcnp  23759  jensen  23779  ppisval  23893  chtlepsi  23997  chpub  24011  edgss  24925  chssoc  26984  mdsl0  27798  mdexchi  27823  atcvat3i  27884  dmdbr5ati  27910  funimass4f  28074  xrofsup  28189  locfinreflem  28506  cmpcref  28516  cnvordtrestixx  28558  ordtrestNEW  28566  ordtrest2NEW  28568  pnfneige0  28596  sigagenss  28810  imambfm  28923  dya2iocress  28935  dya2icoseg  28938  dya2iocucvr  28945  ballotlemro  29181  bnj1097  29578  bnj1452  29649  cvmlift3lem6  29835  msubrn  29955  mclsssv  29990  mclsind  29996  trpredmintr  30259  nobndlem8  30373  liness  30697  neibastop2lem  30801  opnmbllem0  31680  mblfinlem2  31682  isbndx  31818  isbnd2  31819  ssbnd  31824  heiborlem3  31849  igenmin  32001  lsatlss  32271  lsmsat  32283  lsatfixedN  32284  lssats  32287  lpssat  32288  lssatle  32290  lssat  32291  lsatcvat3  32327  paddssat  33088  paddasslem17  33110  pmodlem2  33121  hlmod1i  33130  pl42lem4N  33256  diassdvaN  34337  dia2dimlem10  34350  cdlemn4a  34476  cdlemn5pre  34477  dihord5apre  34539  lclkrlem2e  34788  lclkrlem2p  34799  lclkrlem2v  34805  lclkrslem2  34815  lclkrs  34816  lcfrlem25  34844  lcfrlem35  34854  mapdval2N  34907  mapdpglem8  34956  mapdpglem13  34961  baerlem3lem2  34987  mapdindp2  34998  hdmap11lem2  35122  elrfi  35245  isnacs3  35261  mzpf  35287  mzpindd  35297  diophrw  35310  eldiophss  35326  rmxyelqirr  35464  pw2f1ocnv  35598  aomclem6  35623  hbt  35695  rgspnmin  35736  dfrcl2  35905  fvmptiunrelexplb0da  35916  relexp0a  35947  cotrcltrcl  35956  trclimalb2  35957  cotrclrcl  35973  fnresdmss  37053  mptelpm  37063  mptss  37078  founiiun0  37088  uzfissfz  37158  iuneqfzuzlem  37166  icccncfext  37337  dvnprodlem1  37390  dvnprodlem2  37391  dvnprodlem3  37392  fourierdlem41  37579  fourierdlem70  37608  fourierdlem71  37609  fourierdlem80  37618  fourierdlem113  37651  iundjiun  37807  meadjiunlem  37812  meaiunlelem  37815  omeunle  37846  carageniuncllem2  37852  caratheodorylem1  37856  caratheodorylem2  37857  linc1  38978
  Copyright terms: Public domain W3C validator