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

Theorem sseq1d 3375
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 3369 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    C_ wss 3320
This theorem is referenced by:  sseq12d  3377  eqsstrd  3382  snssg  3932  ssiun2s  4135  disjxiun  4209  treq  4308  funimass1  5526  feq1  5576  fvmptss  5813  fvimacnvi  5844  fvimacnvALT  5849  fnsuppres  5952  knatar  6080  ovmptss  6428  oaordi  6789  oaword2  6796  oawordeulem  6797  omword1  6816  oewordri  6835  oeordsuc  6837  nnaordi  6861  nnawordex  6880  ereq1  6912  elpm2r  7034  inficl  7430  fipwss  7434  dffi3  7436  hartogslem1  7511  inf3lema  7579  inf3lemd  7582  cantnfle  7626  cantnflem2  7646  trcl  7664  tcmin  7680  rankr1ai  7724  rankxplim  7803  scottex  7809  scott0  7810  scottexs  7811  scott0s  7812  karden  7819  cardne  7852  cardaleph  7970  ackbij2  8123  cflim2  8143  cfslb  8146  coftr  8153  fin23lem15  8214  fin23lem32  8224  fin23lem34  8226  fin23lem35  8227  fin23lem36  8228  fin23lem41  8232  isf32lem1  8233  itunitc1  8300  axdc3lem2  8331  ttukeylem1  8389  fpwwe2cbv  8505  fpwwe2lem2  8507  fpwwe2  8518  fpwwecbv  8519  fpwwelem  8520  canthwelem  8525  canthwe  8526  wunex2  8613  wuncval2  8622  eltsk2g  8626  tskpwss  8627  inar1  8650  grothpw  8701  grothpwex  8702  axgroth6  8703  grothac  8705  peano5uzti  10359  lo1o1  12326  o1lo1  12331  o1lo12  12332  lo1eq  12362  rlimeq  12363  isercoll  12461  prmreclem4  13287  vdwmc  13346  vdwlem1  13349  vdwlem2  13350  vdwlem12  13360  vdwlem13  13361  ramval  13376  ramz2  13392  ramub1lem1  13394  isacs2  13878  isacs1i  13882  mreacs  13883  acsfn  13884  rescabs  14033  ipole  14584  ipodrsima  14591  isacs5  14598  sylow1  15237  efgval2  15356  efgsfo  15371  frgpuplem  15404  dprdcntz  15566  islbs2  16226  pptbas  17072  pnfnei  17284  mnfnei  17285  iscnp  17301  iscnp4  17327  cnntr  17339  cnconst2  17347  cnpresti  17352  cnprest  17353  isreg  17396  isnrm  17399  isnrm2  17422  perfcls  17429  isreg2  17441  hauscmplem  17469  1stcfb  17508  1stcelcls  17524  1stccnp  17525  txbas  17599  ptbasfi  17613  xkoopn  17621  xkoccn  17651  txcnp  17652  ptcnplem  17653  txdis  17664  txdis1cn  17667  txtube  17672  txkgen  17684  xkohaus  17685  xkoptsub  17686  xkoco1cn  17689  xkoco2cn  17690  xkococnlem  17691  xkococn  17692  xkoinjcn  17719  kqreglem1  17773  kqreglem2  17774  kqnrmlem1  17775  kqnrmlem2  17776  reghmph  17825  nrmhmph  17826  trfil2  17919  ufileu  17951  elfm  17979  elfm2  17980  elfm3  17982  imaelfm  17983  rnelfm  17985  fmfnfmlem2  17987  fmfnfmlem4  17989  fmco  17993  elflim2  17996  flffbas  18027  lmflf  18037  txflf  18038  fclscf  18057  flimfnfcls  18060  cnextcn  18098  symgtgp  18131  ghmcnp  18144  divstgplem  18150  eltsms  18162  ustval  18232  ust0  18249  trust  18259  utoptop  18264  restutop  18267  restutopopn  18268  utopsnneiplem  18277  ucncn  18315  fmucnd  18322  cfilufg  18323  trcfilu  18324  neipcfilu  18326  blssps  18454  blss  18455  ssblex  18458  blin2  18459  metss2  18542  metrest  18554  metcnp3  18570  metustexhalfOLD  18593  metustexhalf  18594  metustblOLD  18610  metustbl  18611  metutopOLD  18612  psmetutop  18613  xrsmopn  18843  recld2  18845  icccmplem1  18853  icccmplem2  18854  icccmp  18856  reconnlem2  18858  lebnumlem3  18988  lebnum  18989  xlebnum  18990  lebnumii  18991  nmhmcn  19128  cfilfval  19217  caubl  19260  caublcls  19261  bcthlem1  19277  bcth  19282  ovolfiniun  19397  ovoliunlem3  19400  ovoliun  19401  ovoliun2  19402  ovoliunnul  19403  voliunlem3  19446  dyadmax  19490  dyadmbllem  19491  dyadmbl  19492  opnmbllem  19493  ellimc2  19764  limcnlp  19765  ellimc3  19766  limcflf  19768  limciun  19781  cpnord  19821  lhop  19900  xrlimcnp  20807  cvxcl  20823  dchrval  21018  isssp  22223  ubthlem1  22372  shmodi  22892  chsupid  22914  chsscon3  23002  spansncvi  23154  mdslmd1lem3  23830  mdslmd1lem4  23831  mdsymlem5  23910  dmdbr5ati  23925  dmdbr6ati  23926  dmdbr7ati  23927  ssiun2sf  24010  tpr2rico  24310  pnfneige0  24336  rrhre  24387  dya2icoseg2  24628  kur14  24902  cvmliftlem15  24985  cvmlift2lem12  25001  cvmlift2lem13  25002  relexpdm  25135  relexprn  25136  rtrclreclem.min  25147  dfrtrcl2  25148  dfpo2  25378  preddowncl  25471  trpredlem1  25505  trpredmintr  25509  wrecseq123  25532  wfrlem1  25538  wfrlem3  25540  wfrlem9  25546  wfrlem15  25552  frrlem1  25582  frrlem4  25585  frrlem5e  25590  nobndup  25655  nobnddown  25656  nofulllem5  25661  opnmbllem0  26242  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  ovoliunnfl  26248  ex-ovoliunnfl  26249  voliunnfl  26250  opnrebl  26323  opnrebl2  26324  ivthALT  26338  neibastop2lem  26389  fnemeet1  26395  filnetlem1  26407  filnetlem4  26410  totbndbnd  26498  heibor1lem  26518  heiborlem10  26529  ismrcd1  26752  nacsfix  26766  setindtr  27095  frlmssuvc1  27223  frlmssuvc2  27224  frlmsslsp  27225  hbtlem6  27310  symgsssg  27385  psgnunilem5  27394  frgraunss  28385  frgra1v  28388  frgra2v  28389  frgra3vlem1  28390  frgra3vlem2  28391  frgra3v  28392  4cycl2vnunb  28407  n4cyclfrgra  28408  bnj517  29256  bnj1014  29331  bnj1015  29332  bnj1123  29355  bnj1125  29361  bnj1450  29419  bnj1452  29421  lcv1  29839  lfl1dim  29919  lfl1dim2N  29920  paddasslem17  30633  dihglblem6  32138  dochvalr  32155  dochord3  32170  lpolconN  32285  lcfls1lem  32332  mapdffval  32424  mapdfval  32425  mapdsn2  32440  mapd0  32463  lspindp5  32568  mapdh8ab  32575
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator