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

Theorem eqsstrd 3374
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 3367 . 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 1652    C_ wss 3312
This theorem is referenced by:  eqsstr3d  3375  syl6eqss  3390  tfisi  4830  suppssof1  6338  riotassuni  6580  onfununi  6595  oawordeulem  6789  oeeui  6837  nnawordex  6872  oaabslem  6878  oaabs2  6880  omabslem  6881  omabs  6882  pw2f1olem  7204  fodomr  7250  fival  7409  dffi3  7428  ordtypelem7  7485  ordtypelem8  7486  wemapso2  7513  cantnflt2  7620  mapfien  7645  tcss  7675  tcel  7676  r1val1  7704  rankuni2b  7771  tcrank  7800  cardonle  7836  harval2  7876  carduniima  7969  ackbij2  8115  cfub  8121  cflecard  8125  cfflb  8131  isf32lem8  8232  itunitc1  8292  ttukeylem7  8387  fpwwe2lem9  8505  wuncss  8612  wuncval2  8614  grur1a  8686  limsupgre  12267  isercolllem3  12452  4sqlem19  13323  vdwlem1  13341  vdwlem12  13352  ramub1lem1  13386  ressress  13518  imasaddfnlem  13745  imasaddflem  13747  imasvscafn  13754  imasvscaf  13756  imasless  13757  isohom  13989  ressffth  14127  acsfiindd  14595  acsmap2d  14597  dirref  14672  sylow2alem2  15244  lsmssv  15269  lsmidm  15288  gsumzres  15509  dprdlub  15576  dprdf1  15583  dprdsn  15586  dprdcntz2  15588  dprd2dlem1  15591  dprd2da  15592  dmdprdsplit2lem  15595  ablfac1eu  15623  drnglpir  16316  issubassa2  16395  evlslem4  16556  znleval  16827  lpsscls  17197  tgrest  17215  resttopon  17217  rest0  17225  restfpw  17235  ordtrest  17258  ordtrest2  17260  lmcnp  17360  tgcmp  17456  uncmp  17458  hauscmplem  17461  1stcfb  17500  2ndcdisj  17511  kgencmp  17569  xkouni  17623  prdstopn  17652  txtube  17664  txcmplem2  17666  xkoptsub  17678  xkopt  17679  xkococnlem  17683  qtoprest  17741  imastopn  17744  kqdisj  17756  reghmph  17817  nrmhmph  17818  fbssfi  17861  trfilss  17913  trfg  17915  elfm3  17974  alexsubALTlem3  18072  alexsubALT  18074  cnextf  18089  cnextcn  18090  clsnsg  18131  tgpconcompeqg  18133  divstgphaus  18144  trust  18251  ustuqtop3  18265  neipcfilu  18318  metequiv2  18532  prdsxmslem2  18551  metustfbasOLD  18587  metustfbas  18588  icccmplem1  18845  metdstri  18873  pi1addf  19064  pi1addval  19065  caubl  19252  caublcls  19253  relcmpcmet  19261  minveclem4  19325  hlhil  19336  ovolficcss  19358  uniioombllem3a  19468  uniioombllem3  19469  dyadss  19478  opnmbllem  19485  i1fima2  19563  limcfval  19751  dvfval  19776  dvnres  19809  dvivth  19886  lhop  19892  evlseu  19929  taylf  20269  xrlimcnp  20799  jensen  20819  ppisval  20878  chtlepsi  20982  chpub  20996  chssoc  22990  mdsl0  23805  mdexchi  23830  atcvat3i  23891  dmdbr5ati  23917  funimass4f  24036  xrofsup  24118  cnvordtrestixx  24303  pnfneige0  24328  sigagenss  24524  imambfm  24604  dya2iocress  24616  dya2icoseg  24619  dya2iocucvr  24626  ballotlemro  24772  cvmlift3lem6  25003  relexpfld  25129  rtrclreclem.min  25139  trpredmintr  25501  nobndlem8  25646  liness  26071  mblfinlem  26234  neibastop2lem  26380  isbndx  26482  isbnd2  26483  ssbnd  26488  heiborlem3  26513  igenmin  26665  elrfi  26739  isnacs3  26755  mzpf  26784  mzpindd  26794  diophrw  26808  eldiophss  26824  rmxyelqirr  26964  pw2f1ocnv  27099  aomclem6  27125  frlmsplit2  27211  f1lindf  27260  hbt  27302  rgspnmin  27344  f1omvdco2  27359  pmtrfrn  27368  symgsssg  27376  symggen  27379  psgnunilem1  27384  bnj1097  29287  bnj1452  29358  lsatlss  29731  lsmsat  29743  lsatfixedN  29744  lssats  29747  lpssat  29748  lssatle  29750  lssat  29751  lsatcvat3  29787  paddssat  30548  paddasslem17  30570  pmodlem2  30581  hlmod1i  30590  pl42lem4N  30716  diassdvaN  31795  dia2dimlem10  31808  cdlemn4a  31934  cdlemn5pre  31935  dihord5apre  31997  lclkrlem2e  32246  lclkrlem2p  32257  lclkrlem2v  32263  lclkrslem2  32273  lclkrs  32274  lcfrlem25  32302  lcfrlem35  32312  mapdval2N  32365  mapdpglem8  32414  mapdpglem13  32419  baerlem3lem2  32445  mapdindp2  32456  hdmap11lem2  32580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator