Theorem sseq1d 3953

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq1d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Proof of Theorem sseq1d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq1 3947	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseq12d  3955  eqsstrd  3956  ssiun2s  4985  disjxiun  5076  treq  5193  iunopeqop  5469  iunopeqopOLD  5470  dfpo2  6254  preddowncl  6290  funimass1  6574  f1imadifssran  6578  feq1  6640  focofo  6759  fvmptss  6955  fvimacnvi  7000  fvimacnvALT  7005  knatar  7308  ovmptss  8039  fnsuppres  8138  frecseq123  8229  csbfrecsg  8231  frrlem1  8233  frrlem3  8235  frrlem4  8236  frrlem13  8245  frrdmcl  8255  fprresex  8257  dfrecs3  8309  oaordi  8478  oaword2  8485  oawordeulem  8486  omword1  8505  oewordri  8525  oeordsuc  8527  nnaordi  8551  nnawordex  8570  naddcllem  8609  naddunif  8626  ereq1  8648  elpm2r  8789  inficl  9335  fipwss  9339  dffi3  9341  hartogslem1  9454  inf3lema  9543  inf3lemd  9546  cantnfle  9590  cantnflem2  9609  ttrclselem1  9644  trcl  9647  tcmin  9658  rankr1ai  9720  rankxplim  9801  scottex  9807  scott0  9808  scottexs  9809  scott0s  9810  karden  9817  cardne  9887  cardaleph  10009  ackbij2  10162  cflim2  10183  cfslb  10186  coftr  10193  fin23lem15  10254  fin23lem32  10264  fin23lem34  10266  fin23lem35  10267  fin23lem36  10268  fin23lem41  10272  isf32lem1  10273  itunitc1  10340  axdc3lem2  10371  ttukeylem1  10429  fpwwe2cbv  10551  fpwwe2lem2  10553  fpwwe2lem4  10555  fpwwe2  10564  fpwwecbv  10565  fpwwelem  10566  canthwelem  10571  canthwe  10572  pwfseqlem4  10583  wunex2  10659  wuncval2  10668  eltsk2g  10672  tskpwss  10673  inar1  10696  grothpw  10747  grothpwex  10748  axgroth6  10749  grothac  10751  peano5uzti  12617  fsuppmapnn0fiub0  13953  relexpnndm  15001  rtrclreclem4  15021  dfrtrcl2  15022  lo1o1  15492  o1lo1  15497  o1lo12  15498  lo1eq  15528  rlimeq  15529  isercoll  15628  prmreclem4  16888  vdwmc  16947  vdwlem1  16950  vdwlem2  16951  vdwlem12  16961  vdwlem13  16962  ramval  16977  ramz2  16993  ramub1lem1  16995  isacs2  17617  isacs1i  17621  mreacs  17622  acsfn  17623  rescabs  17798  ipole  18498  ipodrsima  18505  isacs5  18512  symgsssg  19440  psgnunilem5  19467  sylow1  19576  efgval2  19697  efgsfo  19712  frgpuplem  19745  gsumzf1o  19885  gsumzoppg  19917  dprdcntz  19983  islbs2  21154  frlmssuvc1  21776  frlmssuvc2  21777  frlmsslsp  21778  ismhp  22135  pptbas  22998  pnfnei  23210  mnfnei  23211  iscnp  23227  iscnp4  23253  cnntr  23265  cnconst2  23273  cnpresti  23278  cnprest  23279  isreg  23322  isnrm  23325  isnrm2  23348  perfcls  23355  isreg2  23367  hauscmplem  23396  1stcfb  23435  1stcelcls  23451  1stccnp  23452  txbas  23557  ptbasfi  23571  xkoopn  23579  xkoccn  23609  txcnp  23610  ptcnplem  23611  txdis  23622  txdis1cn  23625  txtube  23630  txkgen  23642  xkohaus  23643  xkoptsub  23644  xkoco1cn  23647  xkoco2cn  23648  xkococnlem  23649  xkococn  23650  xkoinjcn  23677  kqreglem1  23731  kqreglem2  23732  kqnrmlem1  23733  kqnrmlem2  23734  reghmph  23783  nrmhmph  23784  trfil2  23877  ufileu  23909  elfm  23937  elfm2  23938  elfm3  23940  imaelfm  23941  rnelfm  23943  fmfnfmlem2  23945  fmfnfmlem4  23947  fmco  23951  elflim2  23954  flffbas  23985  lmflf  23995  txflf  23996  fclscf  24015  flimfnfcls  24018  cnextcn  24057  symgtgp  24096  ghmcnp  24105  qustgplem  24111  eltsms  24123  ustval  24193  ust0  24210  trust  24219  utoptop  24224  restutop  24227  restutopopn  24228  utopsnneiplem  24237  ucncn  24274  fmucnd  24281  cfilufg  24282  trcfilu  24283  neipcfilu  24285  blssps  24414  blss  24415  ssblex  24418  blin2  24419  metss2  24502  metrest  24514  metcnp3  24530  metustexhalf  24546  metustbl  24556  psmetutop  24557  xrsmopn  24803  recld2  24805  icccmplem1  24813  icccmplem2  24814  icccmp  24816  reconnlem2  24818  lebnumlem3  24955  lebnum  24956  xlebnum  24957  lebnumii  24958  nmhmcn  25112  cfilfval  25256  caubl  25300  caublcls  25301  bcthlem1  25316  bcth  25321  ovolfiniun  25493  ovoliunlem3  25496  ovoliun  25497  ovoliun2  25498  ovoliunnul  25499  voliunlem3  25544  dyadmax  25590  dyadmbllem  25591  dyadmbl  25592  opnmbllem  25593  ellimc2  25869  limcnlp  25870  ellimc3  25871  limcflf  25873  limciun  25886  cpnord  25927  lhop  26008  xrlimcnp  26957  cvxcl  26973  dchrval  27222  noetalem2  27731  madebdayim  27905  madebdaylemold  27915  madebday  27917  bdayle  27933  precsexlem8  28231  bdaypw2n0bndlem  28480  bdayfinbndcbv  28483  bdayfinbndlem1  28484  bdayfinbndlem2  28485  bdayfinbnd  28486  ausgrumgri  29261  ausgrusgri  29262  nbgrval  29430  nbgrel  29434  nbumgrvtx  29440  nbgrnself  29453  uvtxel1  29490  wlkonl1iedg  29757  crctcshwlkn0lem6  29908  2wlkdlem10  30028  1wlkdlem4  30235  3wlkdlem6  30260  3wlkdlem10  30264  eupth2lem3lem4  30326  frcond1  30361  frgr1v  30366  nfrgr2v  30367  frgr3vlem1  30368  frgr3vlem2  30369  frgr3v  30370  4cycl2vnunb  30385  n4cyclfrgr  30386  isssp  30820  ubthlem1  30966  shmodi  31486  chsupid  31508  chsscon3  31596  spansncvi  31748  mdslmd1lem3  32423  mdslmd1lem4  32424  mdsymlem5  32503  dmdbr5ati  32518  dmdbr6ati  32519  dmdbr7ati  32520  ssiun2sf  32655  fpwrelmapffslem  32831  prodindf  32948  pwrssmgc  33086  fldgenval  33403  unitprodclb  33479  esplysply  33762  esplyfvaln  33765  esplyind  33766  resssra  33778  constrsscn  33931  constrextdg2lem  33939  constrextdg2  33940  txomap  34025  locfinreflem  34031  tpr2rico  34103  pnfneige0  34142  rrhre  34212  dya2icoseg2  34469  omsfval  34485  eulerpartlemt0  34560  eulerpartgbij  34563  eulerpartlemr  34565  eulerpartlemgs2  34571  eulerpartlemn  34572  eulerpart  34573  bnj517  35074  bnj1014  35150  bnj1015  35151  bnj1123  35175  bnj1125  35181  bnj1450  35239  bnj1452  35241  cplgredgex  35356  kur14  35451  cvmliftlem15  35533  cvmlift2lem12  35549  cvmlift2lem13  35550  mclsval  35798  mclsax  35804  mclsppslem  35818  prodeq12sdv  36453  cbvsumdavw2  36530  cbvproddavw2  36531  opnrebl  36555  opnrebl2  36556  ivthALT  36570  neibastop2lem  36595  fnemeet1  36601  filnetlem1  36613  filnetlem4  36616  ttcmin  36731  dfttc2g  36741  bj-imdirval3  37551  bj-imdiridlem  37552  rdgssun  37747  lindsadd  37987  lindsenlbs  37989  ptrecube  37994  poimirlem32  38026  opnmbllem0  38030  mblfinlem1  38031  mblfinlem2  38032  mblfinlem3  38033  ovoliunnfl  38036  ex-ovoliunnfl  38037  voliunnfl  38038  totbndbnd  38163  heibor1lem  38183  heiborlem10  38194  scottexf  38542  scott0f  38543  relcnveq2  38703  cnvref4  38724  dfcnvrefrels2  38982  dfcnvrefrel2  38984  elrelscnveq2  39003  symrefref2  39021  lcv1  39540  lfl1dim  39620  lfl1dim2N  39621  paddasslem17  40335  dihglblem6  41839  dochvalr  41856  dochord3  41871  lpolconN  41986  lcfls1lem  42033  mapdffval  42125  mapdfval  42126  mapdsn2  42141  mapd0  42164  lspindp5  42269  mapdh8ab  42276  primrootscoprbij  42594  aks6d1c2  42622  aks6d1c6lem3  42664  aks6d1c6lem5  42669  aks6d1c7lem1  42672  ismrcd1  43154  nacsfix  43168  setindtr  43476  hbtlem6  43581  oaabsb  43746  tfsconcatrnss  43802  naddwordnexlem4  43853  clcnvlem  44074  iunrelexpmin1  44159  iunrelexpmin2  44163  relexp0a  44167  cotrcltrcl  44176  trclimalb2  44177  cotrclrcl  44193  sbcheg  44230  clsk1indlem1  44496  isotone1  44499  isotone2  44500  ntrclsiso  44518  ntrclsk2  44519  k0004lem1  44598  k0004lem3  44600  scottelrankd  44698  mnuop123d  44713  mnuprdlem1  44723  mnuprdlem2  44724  mnuunid  44728  mnurndlem1  44732  modelaxreplem1  45429  modelaxreplem2  45430  modelaxrep  45432  ssdec  45542  iinssd  45585  iinssdf  45593  ssnnf1octb  45648  iooiinicc  45994  iooiinioc  46008  icccncfext  46337  fourierdlem41  46598  meaiininclem  46936  hoidmvlelem3  47047  hoidmvle  47050  opnvonmbllem1  47082  opnvonmbl  47084  iinhoiicclem  47123  smflim  47227  smflimsuplem7  47276  clnbgrval  48320  clnbgrel  48326  sclnbgrel  48345  isubgredg  48364  isubgruhgr  48366  uhgrimisgrgriclem  48428  uhgrimisgrgric  48429  clnbgrgrimlem  48431  clnbgrgrim  48432  isubgr3stgrlem7  48470  uspgrlimlem1  48486  uspgrlimlem2  48487  uspgrlimlem3  48488  uspgrlim  48490  pgnbgreunbgr  48623  uspgrsprf  48644  iinglb  49319  iscnrm3r  49445  iscnrm3l  49448  imassc  49650  setrecseq  50182  setrec1lem4  50187  setrec2fun  50189