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

Theorem eqsstrd 3477
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 3470 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
41, 3mpbird 240 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454    C_ wss 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429
This theorem is referenced by:  eqsstr3d  3478  syl6eqss  3493  fpr2g  6149  tfisi  6711  suppssof1  6974  suppss2  6975  onfununi  7085  oawordeulem  7280  oeeui  7328  nnawordex  7363  oaabslem  7369  oaabs2  7371  omabslem  7372  omabs  7373  pw2f1olem  7701  fodomr  7748  fival  7951  dffi3  7970  ordtypelem7  8064  ordtypelem8  8065  wemapso2lem  8092  cantnflt2  8203  cantnflem1  8219  tcss  8253  tcel  8254  r1val1  8282  rankuni2b  8349  tcrank  8380  cardonle  8416  harval2  8456  carduniima  8552  ackbij2  8698  cfub  8704  cflecard  8708  cfflb  8714  isf32lem8  8815  itunitc1  8875  ttukeylem7  8970  fpwwe2lem9  9088  wuncss  9195  wuncval2  9197  grur1a  9269  trclfvub  13119  cotrtrclfv  13124  relexpfld  13160  rtrclreclem4  13172  limsupgre  13590  limsupgreOLD  13591  isercolllem3  13778  4sqlem19  14961  vdwlem1  14979  vdwlem12  14990  ramub1lem1  15032  ressress  15235  imasaddfnlem  15482  imasaddflem  15484  imasvscafn  15491  imasvscaf  15493  imasless  15494  isohom  15729  ressffth  15891  acsfiindd  16471  acsmap2d  16473  dirref  16529  mrcmndind  16661  f1omvdco2  17137  pmtrfrn  17147  symgsssg  17156  symggen  17159  psgnunilem1  17182  sylow2alem2  17318  lsmssv  17343  lsmidm  17362  gsumzres  17591  dprdlub  17707  dprdf1  17714  dprdsn  17717  dprdcntz2  17719  dprd2dlem1  17722  dprd2da  17723  dmdprdsplit2lem  17726  ablfac1eu  17754  drnglpir  18525  issubassa2  18617  evlslem4  18779  evlseu  18787  znleval  19173  evpmss  19202  frlmsplit2  19379  f1lindf  19428  lpsscls  20205  tgrest  20223  resttopon  20225  rest0  20233  restfpw  20243  ordtrest  20266  ordtrest2  20268  lmcnp  20368  tgcmp  20464  uncmp  20466  hauscmplem  20469  1stcfb  20508  2ndcdisj  20519  dissnref  20591  kgencmp  20608  xkouni  20662  prdstopn  20691  txtube  20703  txcmplem2  20705  xkoptsub  20717  xkopt  20718  xkococnlem  20722  qtoprest  20780  imastopn  20783  kqdisj  20795  reghmph  20856  nrmhmph  20857  fbssfi  20900  trfilss  20952  trfg  20954  elfm3  21013  alexsubALTlem3  21112  alexsubALT  21114  cnextf  21129  cnextcn  21130  clsnsg  21172  tgpconcompeqg  21174  qustgphaus  21185  trust  21292  ustuqtop3  21306  neipcfilu  21359  metequiv2  21573  prdsxmslem2  21592  metustfbas  21620  icccmplem1  21888  metdstri  21916  metdstriOLD  21931  pi1addf  22126  pi1addval  22127  caubl  22325  caublcls  22326  relcmpcmet  22334  minveclem4  22422  minveclem4OLD  22434  hlhil  22445  ovolficcss  22470  uniioombllem3a  22590  uniioombllem3  22591  dyadss  22600  opnmbllem  22607  i1fima2  22685  limcfval  22875  dvfval  22900  dvnres  22933  dvivth  23010  lhop  23016  taylf  23364  xrlimcnp  23942  jensen  23962  ppisval  24078  chtlepsi  24182  chpub  24196  iscgrglt  24607  edgss  25127  chssoc  27197  mdsl0  28011  mdexchi  28036  atcvat3i  28097  dmdbr5ati  28123  funimass4f  28282  xrofsup  28401  locfinreflem  28715  cmpcref  28725  cnvordtrestixx  28767  ordtrestNEW  28775  ordtrest2NEW  28777  pnfneige0  28805  sigagenss  29019  imambfm  29132  dya2iocress  29144  dya2icoseg  29147  dya2iocucvr  29154  ballotlemro  29403  ballotlemroOLD  29441  bnj1097  29838  bnj1452  29909  cvmlift3lem6  30095  msubrn  30215  mclsssv  30250  mclsind  30256  trpredmintr  30520  nobndlem8  30636  liness  30960  neibastop2lem  31064  opnmbllem0  32020  mblfinlem2  32022  isbndx  32158  isbnd2  32159  ssbnd  32164  heiborlem3  32189  igenmin  32341  lsatlss  32606  lsmsat  32618  lsatfixedN  32619  lssats  32622  lpssat  32623  lssatle  32625  lssat  32626  lsatcvat3  32662  paddssat  33423  paddasslem17  33445  pmodlem2  33456  hlmod1i  33465  pl42lem4N  33591  diassdvaN  34672  dia2dimlem10  34685  cdlemn4a  34811  cdlemn5pre  34812  dihord5apre  34874  lclkrlem2e  35123  lclkrlem2p  35134  lclkrlem2v  35140  lclkrslem2  35150  lclkrs  35151  lcfrlem25  35179  lcfrlem35  35189  mapdval2N  35242  mapdpglem8  35291  mapdpglem13  35296  baerlem3lem2  35322  mapdindp2  35333  hdmap11lem2  35457  elrfi  35580  isnacs3  35596  mzpf  35622  mzpindd  35632  diophrw  35645  eldiophss  35661  rmxyelqirr  35802  pw2f1ocnv  35936  aomclem6  35961  hbt  36033  rgspnmin  36081  cnvssb  36236  trclubgNEW  36269  dfrcl2  36310  fvmptiunrelexplb0da  36321  relexp0a  36352  cotrcltrcl  36361  trclimalb2  36362  cotrclrcl  36378  fnresdmss  37468  mptelpm  37478  mptss  37492  founiiun0  37502  ssnnf1octb  37507  uzfissfz  37586  iuneqfzuzlem  37594  icccncfext  37802  dvnprodlem1  37858  dvnprodlem2  37859  dvnprodlem3  37860  fourierdlem41  38048  fourierdlem70  38077  fourierdlem71  38078  fourierdlem80  38087  fourierdlem113  38120  rrxbasefi  38189  salgenss  38232  dfsalgen2  38237  iundjiun  38335  meadjiunlem  38340  meaiunlelem  38343  omeunle  38374  carageniuncllem2  38380  caratheodorylem1  38384  caratheodorylem2  38385  hoissre  38403  ovnsubaddlem1  38429  hoidmvlelem3  38456  ovnhoilem1  38460  ovnhoilem2  38461  ovnhoi  38462  ovncvr2  38470  voncmpl  38480  hspmbllem2  38486  hspmbl  38488  opnvonmbllem1  38491  uhgredgn0  39267  upgredgss  39270  umgredgss  39271  usgredgss  39294  linc1  40490
  Copyright terms: Public domain W3C validator