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

Theorem sseq2d 3219
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
sseq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sseq2d  |-  ( ph  ->  ( C  C_  A  <->  C 
C_  B ) )

Proof of Theorem sseq2d
StepHypRef Expression
1 sseq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sseq2 3213 . 2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
31, 2syl 15 1  |-  ( ph  ->  ( C  C_  A  <->  C 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    C_ wss 3165
This theorem is referenced by:  sseq12d  3220  sseqtrd  3227  funimass2  5342  fnco  5368  fnssresb  5372  fnimaeq0  5381  foimacnv  5506  fvelimab  5594  ssimaexg  5601  knatar  5873  onfununi  6374  oaordi  6560  oawordeulem  6568  oaass  6575  odi  6593  omass  6594  oen0  6600  oelim2  6609  nnaordi  6632  nnawordex  6651  pssnn  7097  fissuni  7176  dffi3  7200  cantnfle  7388  cantnflem1  7407  trcl  7426  r1sdom  7462  iscard2  7625  alephordi  7717  alephgeom  7725  cardaleph  7732  cardalephex  7733  ackbij2lem4  7884  cflm  7892  cfslbn  7909  cofsmo  7911  cfsmolem  7912  cfcoflem  7914  coftr  7915  alephsing  7918  fin23lem28  7982  fin23lem30  7984  fin23lem33  7987  fin1a2lem9  8050  axdc3lem2  8093  ttukeylem5  8156  fpwwe2lem5  8272  pwfseqlem4a  8299  pwfseqlem4  8300  wunex2  8376  inar1  8413  sstskm  8480  summolem2  12205  summo  12206  zsum  12207  sumz  12211  sumss  12213  fsumcvg3  12218  vdwlem1  13044  vdwlem12  13055  vdwlem13  13056  ramub2  13077  rami  13078  ramz2  13087  prdsval  13371  pwsle  13407  mrcuni  13539  isclat  14231  gsumpropd  14469  gsumress  14470  eqgfval  14681  sscntz  14818  resscntz  14823  lsmlub  14990  efgrelexlemb  15075  efgcpbllemb  15080  gsumval3a  15205  dmdprd  15252  dprdcntz  15259  subgdmdprd  15285  subrgpropd  15595  islss  15708  lsslss  15734  lsspropd  15790  lsmelpr  15860  lbspropd  15868  ltbval  16229  opsrval  16232  isbasisg  16701  tgval  16709  tgss3  16740  restbas  16905  tgrest  16906  restcld  16919  restopn2  16924  restntr  16928  cnpnei  17009  cncls2  17018  perfcls  17109  cmpsublem  17142  cmpsub  17143  cmpcld  17145  uncmp  17146  hauscmplem  17149  cmpfi  17151  nconsubb  17165  clscon  17172  hausllycmp  17236  1stckgenlem  17264  txbas  17278  ptbasfi  17292  txcnpi  17318  ptcnp  17332  txcmplem1  17351  txcmplem2  17352  xkococnlem  17369  qtopcld  17420  fbasssin  17547  fbssint  17549  fbun  17551  fbasrn  17595  filufint  17631  ufinffr  17640  ufildr  17642  elmopn  18004  neibl  18063  icccmplem1  18343  icccmplem2  18344  bndth  18472  isphtpc  18508  metcld  18747  bcthlem1  18762  bcth  18767  ovolfioo  18843  ovolficc  18844  elovolmr  18851  ovoliunlem3  18879  ovolicc2  18897  volsuplem  18928  dyadmax  18969  dyadmbllem  18970  dyadmbl  18971  sspval  21315  ubth  21468  orthin  22041  chssoc  22091  chsscon3  22095  chsscon1  22096  h1datom  22177  pjoml6i  22184  osum  22240  spansncv  22248  pjcjt2  22287  pjopyth  22315  hstel2  22815  hstle  22826  stj  22831  dmdbr5  22904  mdslmd1lem1  22921  atord  22984  chirredlem4  22989  atcvat4i  22993  mdsymlem2  23000  mdsymlem3  23001  mdsymlem8  23006  ssnnssfz  23292  tpr2rico  23311  gsumpropd2lem  23394  sigaval  23486  issiga  23487  issgon  23499  sssigagen  23521  measiuns  23559  kur14  23762  cvmliftlem15  23844  ghomfo  24013  rtrclreclem.refl  24056  rtrclreclem.subset  24057  prodmolem2  24158  prodmo  24159  zprod  24160  prod1  24169  trpredtr  24304  dftrpred3g  24307  wfrlem9  24335  wfrlem12  24338  frrlem5e  24360  nofulllem1  24427  nofulllem2  24428  itgaddnclem2  25010  inpc  25380  basexre  25625  isalg  25824  ivthALT  26361  isfne  26371  topfne  26393  neibastop3  26414  tailfb  26429  filnetlem1  26430  filnetlem4  26433  sstotbnd2  26601  sstotbnd  26602  sstotbnd3  26603  ssbnd  26615  cntotbnd  26623  cnpwstotbnd  26624  ismtyres  26635  heibor1lem  26636  heiborlem1  26638  heiborlem6  26643  heiborlem8  26645  exidreslem  26670  ismrc  26879  incssnn0  26889  nacsfix  26890  lsslinds  27404  hbt  27437  stoweidlem50  27902  stoweidlem57  27909  sbcrel  28084  isfrgra  28417  lshpcmp  29800  lsmsat  29820  lsmsatcv  29822  lfl1dim  29933  lfl1dim2N  29934  lkrss2N  29981  psubspset  30555  paddss  30656  psubclsetN  30747  dilfsetN  30963  dilsetN  30964  diaglbN  31867  dibglbN  31978  dihlspsnat  32145  dihglb2  32154  dochffval  32161  dochfval  32162  dochvalr  32169  dochord2N  32183  dochsncom  32194  dihjat1lem  32240  dvh4dimat  32250  dvh3dimatN  32251  dvh2dimatN  32252  dochexmidlem1  32272  lpolsetN  32294  lpolconN  32299  hdmaplkr  32728  hdmapoc  32746  hlhillcs  32773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator