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

Theorem eqsstrd 3350
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 3343 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 224 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3288
This theorem is referenced by:  eqsstr3d  3351  syl6eqss  3366  tfisi  4805  suppssof1  6313  riotassuni  6555  onfununi  6570  oawordeulem  6764  oeeui  6812  nnawordex  6847  oaabslem  6853  oaabs2  6855  omabslem  6856  omabs  6857  pw2f1olem  7179  fodomr  7225  fival  7383  dffi3  7402  ordtypelem7  7457  ordtypelem8  7458  wemapso2  7485  cantnflt2  7592  mapfien  7617  tcss  7647  tcel  7648  r1val1  7676  rankuni2b  7743  tcrank  7772  cardonle  7808  harval2  7848  carduniima  7941  ackbij2  8087  cfub  8093  cflecard  8097  cfflb  8103  isf32lem8  8204  itunitc1  8264  ttukeylem7  8359  fpwwe2lem9  8477  wuncss  8584  wuncval2  8586  grur1a  8658  limsupgre  12238  isercolllem3  12423  4sqlem19  13294  vdwlem1  13312  vdwlem12  13323  ramub1lem1  13357  ressress  13489  imasaddfnlem  13716  imasaddflem  13718  imasvscafn  13725  imasvscaf  13727  imasless  13728  isohom  13960  ressffth  14098  acsfiindd  14566  acsmap2d  14568  dirref  14643  sylow2alem2  15215  lsmssv  15240  lsmidm  15259  gsumzres  15480  dprdlub  15547  dprdf1  15554  dprdsn  15557  dprdcntz2  15559  dprd2dlem1  15562  dprd2da  15563  dmdprdsplit2lem  15566  ablfac1eu  15594  drnglpir  16287  issubassa2  16366  evlslem4  16527  znleval  16798  lpsscls  17168  tgrest  17185  resttopon  17187  rest0  17195  restfpw  17205  ordtrest  17228  ordtrest2  17230  lmcnp  17330  tgcmp  17426  uncmp  17428  hauscmplem  17431  1stcfb  17469  2ndcdisj  17480  kgencmp  17538  xkouni  17592  prdstopn  17621  txtube  17633  txcmplem2  17635  xkoptsub  17647  xkopt  17648  xkococnlem  17652  qtoprest  17710  imastopn  17713  kqdisj  17725  reghmph  17786  nrmhmph  17787  fbssfi  17830  trfilss  17882  trfg  17884  elfm3  17943  alexsubALTlem3  18041  alexsubALT  18043  cnextf  18058  cnextcn  18059  clsnsg  18100  tgpconcompeqg  18102  divstgphaus  18113  trust  18220  ustuqtop3  18234  neipcfilu  18287  metequiv2  18501  prdsxmslem2  18520  metustfbasOLD  18556  metustfbas  18557  icccmplem1  18814  metdstri  18842  pi1addf  19033  pi1addval  19034  caubl  19221  caublcls  19222  relcmpcmet  19230  minveclem4  19294  hlhil  19305  ovolficcss  19327  uniioombllem3a  19437  uniioombllem3  19438  dyadss  19447  opnmbllem  19454  i1fima2  19532  limcfval  19720  dvfval  19745  dvnres  19778  dvivth  19855  lhop  19861  evlseu  19898  taylf  20238  xrlimcnp  20768  jensen  20788  ppisval  20847  chtlepsi  20951  chpub  20965  chssoc  22959  mdsl0  23774  mdexchi  23799  atcvat3i  23860  dmdbr5ati  23886  funimass4f  24005  xrofsup  24087  cnvordtrestixx  24272  pnfneige0  24297  sigagenss  24493  imambfm  24573  dya2iocress  24585  dya2icoseg  24588  dya2iocucvr  24595  ballotlemro  24741  cvmlift3lem6  24972  relexpfld  25098  rtrclreclem.min  25108  trpredmintr  25456  nobndlem8  25575  liness  25991  mblfinlem  26151  neibastop2lem  26287  isbndx  26389  isbnd2  26390  ssbnd  26395  heiborlem3  26420  igenmin  26572  elrfi  26646  isnacs3  26662  mzpf  26691  mzpindd  26701  diophrw  26715  eldiophss  26731  rmxyelqirr  26871  pw2f1ocnv  27006  aomclem6  27032  frlmsplit2  27119  f1lindf  27168  hbt  27210  rgspnmin  27252  f1omvdco2  27267  pmtrfrn  27276  symgsssg  27284  symggen  27287  psgnunilem1  27292  bnj1097  29068  bnj1452  29139  lsatlss  29491  lsmsat  29503  lsatfixedN  29504  lssats  29507  lpssat  29508  lssatle  29510  lssat  29511  lsatcvat3  29547  paddssat  30308  paddasslem17  30330  pmodlem2  30341  hlmod1i  30350  pl42lem4N  30476  diassdvaN  31555  dia2dimlem10  31568  cdlemn4a  31694  cdlemn5pre  31695  dihord5apre  31757  lclkrlem2e  32006  lclkrlem2p  32017  lclkrlem2v  32023  lclkrslem2  32033  lclkrs  32034  lcfrlem25  32062  lcfrlem35  32072  mapdval2N  32125  mapdpglem8  32174  mapdpglem13  32179  baerlem3lem2  32205  mapdindp2  32216  hdmap11lem2  32340
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator