Theorem sseq1d 3632

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

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 |- ( ph -> A = B )
2		sseq1 3626	. 2 |- ( A = B -> ( A C_ C <-> B C_ C ) )
3	1, 2	syl 17	1 |- ( ph -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseq12d  3634  eqsstrd  3639  snssg  4327  ssiun2s  4564  disjxiun  4649  disjxiunOLD  4650  treq  4758  iunopeqop  4981  preddowncl  5707  funimass1  5971  feq1  6026  fvmptss  6292  fvimacnvi  6331  fvimacnvALT  6336  knatar  6607  ovmptss  7258  fnsuppres  7322  imacosupp  7335  wrecseq123  7408  wfrlem1  7414  wfrlem3  7416  wfrdmcl  7423  wfrlem15  7429  wfrlem17  7431  dfrecs3  7469  oaordi  7626  oaword2  7633  oawordeulem  7634  omword1  7653  oewordri  7672  oeordsuc  7674  nnaordi  7698  nnawordex  7717  ereq1  7749  elpm2r  7875  inficl  8331  fipwss  8335  dffi3  8337  hartogslem1  8447  inf3lema  8521  inf3lemd  8524  cantnfle  8568  cantnflem2  8587  trcl  8604  tcmin  8617  rankr1ai  8661  rankxplim  8742  scottex  8748  scott0  8749  scottexs  8750  scott0s  8751  karden  8758  cardne  8791  cardaleph  8912  ackbij2  9065  cflim2  9085  cfslb  9088  coftr  9095  fin23lem15  9156  fin23lem32  9166  fin23lem34  9168  fin23lem35  9169  fin23lem36  9170  fin23lem41  9174  isf32lem1  9175  itunitc1  9242  axdc3lem2  9273  ttukeylem1  9331  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwe2  9465  fpwwecbv  9466  fpwwelem  9467  canthwelem  9472  canthwe  9473  wunex2  9560  wuncval2  9569  eltsk2g  9573  tskpwss  9574  inar1  9597  grothpw  9648  grothpwex  9649  axgroth6  9650  grothac  9652  peano5uzti  11467  fsuppmapnn0fiub0  12793  relexpnndm  13781  rtrclreclem4  13801  dfrtrcl2  13802  lo1o1  14263  o1lo1  14268  o1lo12  14269  lo1eq  14299  rlimeq  14300  isercoll  14398  prmreclem4  15623  vdwmc  15682  vdwlem1  15685  vdwlem2  15686  vdwlem12  15696  vdwlem13  15697  ramval  15712  ramz2  15728  ramub1lem1  15730  isacs2  16314  isacs1i  16318  mreacs  16319  acsfn  16320  rescabs  16493  ipole  17158  ipodrsima  17165  isacs5  17172  symgsssg  17887  psgnunilem5  17914  sylow1  18018  efgval2  18137  efgsfo  18152  frgpuplem  18185  gsumzf1o  18313  gsumzoppg  18344  dprdcntz  18407  islbs2  19154  frlmssuvc1  20133  frlmssuvc2  20134  frlmsslsp  20135  pptbas  20812  pnfnei  21024  mnfnei  21025  iscnp  21041  iscnp4  21067  cnntr  21079  cnconst2  21087  cnpresti  21092  cnprest  21093  isreg  21136  isnrm  21139  isnrm2  21162  perfcls  21169  isreg2  21181  hauscmplem  21209  1stcfb  21248  1stcelcls  21264  1stccnp  21265  txbas  21370  ptbasfi  21384  xkoopn  21392  xkoccn  21422  txcnp  21423  ptcnplem  21424  txdis  21435  txdis1cn  21438  txtube  21443  txkgen  21455  xkohaus  21456  xkoptsub  21457  xkoco1cn  21460  xkoco2cn  21461  xkococnlem  21462  xkococn  21463  xkoinjcn  21490  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  reghmph  21596  nrmhmph  21597  trfil2  21691  ufileu  21723  elfm  21751  elfm2  21752  elfm3  21754  imaelfm  21755  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmco  21765  elflim2  21768  flffbas  21799  lmflf  21809  txflf  21810  fclscf  21829  flimfnfcls  21832  cnextcn  21871  symgtgp  21905  ghmcnp  21918  qustgplem  21924  eltsms  21936  ustval  22006  ust0  22023  trust  22033  utoptop  22038  restutop  22041  restutopopn  22042  utopsnneiplem  22051  ucncn  22089  fmucnd  22096  cfilufg  22097  trcfilu  22098  neipcfilu  22100  blssps  22229  blss  22230  ssblex  22233  blin2  22234  metss2  22317  metrest  22329  metcnp3  22345  metustexhalf  22361  metustbl  22371  psmetutop  22372  xrsmopn  22615  recld2  22617  icccmplem1  22625  icccmplem2  22626  icccmp  22628  reconnlem2  22630  lebnumlem3  22762  lebnum  22763  xlebnum  22764  lebnumii  22765  nmhmcn  22920  cfilfval  23062  caubl  23106  caublcls  23107  bcthlem1  23121  bcth  23126  ovolfiniun  23269  ovoliunlem3  23272  ovoliun  23273  ovoliun2  23274  ovoliunnul  23275  voliunlem3  23320  dyadmax  23366  dyadmbllem  23367  dyadmbl  23368  opnmbllem  23369  ellimc2  23641  limcnlp  23642  ellimc3  23643  limcflf  23645  limciun  23658  cpnord  23698  lhop  23779  xrlimcnp  24695  cvxcl  24711  dchrval  24959  ausgrumgri  26062  ausgrusgri  26063  nbgrval  26234  nbgrel  26238  nbumgrvtx  26242  nbgrnself  26257  uvtxael1  26296  wlkonl1iedg  26561  crctcshwlkn0lem6  26707  2wlkdlem10  26831  1wlkdlem4  27000  3wlkdlem6  27025  3wlkdlem10  27029  eupth2lem3lem4  27091  frcond1  27130  frgr1v  27135  nfrgr2v  27136  frgr3vlem1  27137  frgr3vlem2  27138  frgr3v  27139  4cycl2vnunb  27154  n4cyclfrgr  27155  isssp  27579  ubthlem1  27726  shmodi  28249  chsupid  28271  chsscon3  28359  spansncvi  28511  mdslmd1lem3  29186  mdslmd1lem4  29187  mdsymlem5  29266  dmdbr5ati  29281  dmdbr6ati  29282  dmdbr7ati  29283  ssiun2sf  29378  fpwrelmapffslem  29507  txomap  29901  locfinreflem  29907  tpr2rico  29958  pnfneige0  29997  rrhre  30065  prodindf  30085  dya2icoseg2  30340  omsfval  30356  eulerpartlemt0  30431  eulerpartgbij  30434  eulerpartlemr  30436  eulerpartlemgs2  30442  eulerpartlemn  30443  eulerpart  30444  bnj517  30955  bnj1014  31030  bnj1015  31031  bnj1123  31054  bnj1125  31060  bnj1450  31118  bnj1452  31120  kur14  31198  cvmliftlem15  31280  cvmlift2lem12  31296  cvmlift2lem13  31297  mclsval  31460  mclsax  31466  mclsppslem  31480  dfpo2  31645  trpredlem1  31727  trpredmintr  31731  frrlem1  31780  frrlem4  31783  frrlem5e  31788  noetalem5  31867  opnrebl  32315  opnrebl2  32316  ivthALT  32330  neibastop2lem  32355  fnemeet1  32361  filnetlem1  32373  filnetlem4  32376  csbwrecsg  33173  lindsenlbs  33404  ptrecube  33409  poimirlem32  33441  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  ovoliunnfl  33451  ex-ovoliunnfl  33452  voliunnfl  33453  totbndbnd  33588  heibor1lem  33608  heiborlem10  33619  scottexf  33976  scott0f  33977  relcnveq2  34094  lcv1  34328  lfl1dim  34408  lfl1dim2N  34409  paddasslem17  35122  dihglblem6  36629  dochvalr  36646  dochord3  36661  lpolconN  36776  lcfls1lem  36823  mapdffval  36915  mapdfval  36916  mapdsn2  36931  mapd0  36954  lspindp5  37059  mapdh8ab  37066  ismrcd1  37261  nacsfix  37275  setindtr  37591  hbtlem6  37699  clcnvlem  37930  iunrelexpmin1  38000  iunrelexpmin2  38004  relexp0a  38008  cotrcltrcl  38017  trclimalb2  38018  cotrclrcl  38034  sbcheg  38073  clsk1indlem1  38343  isotone1  38346  isotone2  38347  ntrclsiso  38365  ntrclsk2  38366  k0004lem1  38445  k0004lem3  38447  ssdec  39265  iinssd  39314  iinssdf  39328  ssnnf1octb  39382  iooiinicc  39769  iooiinioc  39783  icccncfext  40100  fourierdlem41  40365  meaiininclem  40700  hoidmvlelem3  40811  hoidmvle  40814  opnvonmbllem1  40846  opnvonmbl  40848  iinhoiicclem  40887  smflim  40985  smflimsuplem7  41032  uspgrsprf  41754  dfrngc2  41972  setrecseq  42432  setrec1lem4  42437  setrec2fun  42439