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

Theorem sseq1d 3205
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
sseq1d  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )

Proof of Theorem sseq1d
StepHypRef Expression
1 sseq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sseq1 3199 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 15 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    C_ wss 3152
This theorem is referenced by:  sseq12d  3207  eqsstrd  3212  snssg  3754  ssiun2s  3946  disjxiun  4020  treq  4119  dmxpss  5107  iotassuni  5235  funimass1  5325  feq1  5375  fvmptss  5609  fvimacnvi  5639  fvimacnvALT  5644  fnsuppres  5732  knatar  5857  ovmptss  6200  tposss  6235  oaordi  6544  oaword2  6551  oawordeulem  6552  omwordri  6570  omword1  6571  oewordri  6590  oeordsuc  6592  nnaordi  6616  nnawordex  6635  ereq1  6667  elpm2r  6788  map0e  6805  sbthlem5  6975  fodomr  7012  inficl  7178  fipwuni  7179  fipwss  7182  dffi3  7184  ordtypelem6  7238  hartogslem1  7257  inf3lema  7325  inf3lemd  7328  cantnfle  7372  cantnflem2  7392  trcl  7410  tcmin  7426  rankr1ai  7470  rankxplim  7549  scottex  7555  scott0  7556  scottexs  7557  scott0s  7558  karden  7565  cardne  7598  cardaleph  7716  ackbij2  7869  cfub  7875  cflecard  7879  cfle  7880  cflim2  7889  cfslb  7892  coftr  7899  fin23lem15  7960  fin23lem29  7967  fin23lem32  7970  fin23lem34  7972  fin23lem35  7973  fin23lem36  7974  fin23lem41  7978  isf32lem1  7979  compsscnvlem  7996  itunitc1  8046  axdc3lem2  8077  ttukeylem1  8136  fpwwe2cbv  8252  fpwwe2lem2  8254  fpwwe2  8265  fpwwecbv  8266  fpwwelem  8267  canthwelem  8272  canthwe  8273  wunex2  8360  wuncval2  8369  eltsk2g  8373  tskpwss  8374  inar1  8397  grur1a  8441  grothpw  8448  grothpwex  8449  axgroth6  8450  grothac  8452  peano5uzti  10101  lo1o1  12006  o1lo1  12011  o1lo12  12012  lo1eq  12042  rlimeq  12043  isercoll  12141  sadcaddlem  12648  sadcl  12653  smupvallem  12674  smucl  12675  prmreclem4  12966  vdwmc  13025  vdwlem1  13028  vdwlem2  13029  vdwlem12  13039  vdwlem13  13040  ramval  13055  ramz2  13071  ramub1lem1  13073  strfvss  13166  prdsless  13362  isacs2  13555  isacs1i  13559  mreacs  13560  acsfn  13561  rescabs  13710  ipole  14261  ipodrsima  14268  isacs5  14275  sylow1  14914  efgval2  15033  efgsfo  15048  frgpuplem  15081  dprdcntz  15243  islbs2  15907  resspsrbas  16159  resspsrvsca  16162  subrgpsr  16163  ressmplbas  16200  subrgmpl  16204  ressply1bas  16307  cssss  16585  basdif0  16691  pptbas  16745  ordtbas2  16921  ordtbas  16922  pnfnei  16950  mnfnei  16951  iscnp  16967  cnclsi  17001  cncls  17003  cnntr  17004  cnconst2  17011  cnpresti  17016  cnprest  17017  isreg  17060  isnrm  17063  isnrm2  17086  perfcls  17093  isreg2  17105  hauscmplem  17133  cmpfi  17135  1stcfb  17171  1stcelcls  17187  1stccnp  17188  txbas  17262  ptbasfi  17276  xkoopn  17284  txss12  17300  txbasval  17301  xkoccn  17313  txcnp  17314  ptcnplem  17315  prdstopn  17322  txdis  17326  txdis1cn  17329  txtube  17334  txkgen  17346  xkohaus  17347  xkoptsub  17348  xkoco1cn  17351  xkoco2cn  17352  xkococnlem  17353  xkococn  17354  xkoinjcn  17381  kqsat  17422  kqcldsat  17424  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  reghmph  17484  nrmhmph  17485  trfil2  17582  ufileu  17614  elfm  17642  elfm2  17643  elfm3  17645  imaelfm  17646  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmco  17656  elflim2  17659  flffbas  17690  lmflf  17700  txflf  17701  fclscf  17720  flimfnfcls  17723  symgtgp  17784  ghmcnp  17797  divstgplem  17803  eltsms  17815  blss  17972  ssblex  17974  blin2  17975  setsmstopn  18024  metss2  18058  metrest  18070  metcnp3  18086  tngtopn  18166  xrsmopn  18318  recld2  18320  icccmplem1  18327  icccmplem2  18328  icccmp  18330  reconnlem2  18332  metdstri  18355  lebnumlem3  18461  lebnum  18462  xlebnum  18463  lebnumii  18464  nmhmcn  18601  cphsubrglem  18613  tchcph  18667  cfilfval  18690  caubl  18733  caublcls  18734  bcthlem1  18746  bcth  18751  ovolfiniun  18860  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  ovoliunnul  18866  voliunlem3  18909  uniioombllem2  18938  dyadmax  18953  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  ellimc2  19227  limcnlp  19228  ellimc3  19229  limcflf  19231  limciun  19244  cpnord  19284  lhop  19363  dvfsumle  19368  dvfsumabs  19370  xrlimcnp  20263  cvxcl  20279  dchrval  20473  dchrelbas2  20476  subgornss  20973  isssp  21300  ubthlem1  21449  ocsh  21862  shmodi  21969  chsupid  21991  chsupsn  21992  chsscon3  22079  spansncvi  22231  pj3i  22788  mdslmd1lem3  22907  mdslmd1lem4  22908  mdsymlem5  22987  sumdmdlem2  22999  dmdbr5ati  23002  dmdbr6ati  23003  dmdbr7ati  23004  ssiun2sf  23157  tpr2rico  23296  pnfneige0  23374  isibfm  23593  kur14lem1  23737  kur14  23747  cvmliftlem15  23829  cvmlift2lem12  23845  cvmlift2lem13  23846  relexpdm  24032  relexprn  24033  rtrclreclem.min  24044  dfrtrcl2  24045  dfpo2  24112  preddowncl  24196  trpredlem1  24230  trpredmintr  24234  wfrlem1  24256  wfrlem3  24258  wfrlem9  24264  wfrlem15  24270  tfrALTlem  24276  frrlem1  24281  frrlem4  24284  frrlem5e  24289  nobndup  24354  nobnddown  24355  nofulllem5  24360  bpolyval  24784  tpssg  24932  preoref22  25229  osneisi  25531  iscnp4  25563  limptlimpr2lem2  25575  flfnei2  25577  altretop  25600  iintlem2  25611  isalg  25721  algi  25727  tartarmap  25888  pfsubkl  26047  lineval12a  26084  opnrebl  26235  opnrebl2  26236  ivthALT  26258  neibastop2lem  26309  fnemeet1  26315  filnetlem1  26327  filnetlem4  26330  isbnd3  26508  totbndbnd  26513  heibor1lem  26533  heiborlem10  26544  ismrcd1  26773  nacsfix  26787  setindtr  27117  frlmssuvc1  27246  frlmssuvc2  27247  frlmsslsp  27248  hbtlem6  27333  symgsssg  27408  psgnunilem5  27417  frgra1v  28176  frgra2v  28177  frgra3vlem1  28178  frgra3vlem2  28179  frgra3v  28180  bnj517  28917  bnj1014  28992  bnj1015  28993  bnj1123  29016  bnj1125  29022  bnj1450  29080  bnj1452  29082  lcv1  29231  lfl1dim  29311  lfl1dim2N  29312  paddasslem17  30025  dihglblem6  31530  dochvalr  31547  dochord3  31562  lpolconN  31677  lcfls1lem  31724  mapdffval  31816  mapdfval  31817  mapdsn2  31832  mapd0  31855  lspindp5  31960  mapdh8ab  31967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator