Theorem sseq1d 3971

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 3965	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  sseq12d  3973  eqsstrd  3974  ssiun2s  5018  disjxiun  5111  treq  5230  iunopeqop  5509  iunopeqopOLD  5510  dfpo2  6304  preddowncl  6340  funimass1  6625  feq1  6690  focofo  6812  fvmptss  7009  fvimacnvi  7054  fvimacnvALT  7059  knatar  7368  ovmptss  8097  fnsuppres  8196  frecseq123  8288  csbfrecsg  8290  frrlem1  8292  frrlem3  8294  frrlem4  8295  frrlem13  8304  frrdmcl  8314  fprresex  8316  dfrecs3  8368  oaordi  8540  oaword2  8547  oawordeulem  8548  omword1  8567  oewordri  8587  oeordsuc  8589  nnaordi  8613  nnawordex  8632  naddcllem  8671  naddunif  8689  ereq1  8711  elpm2r  8851  inficl  9395  fipwss  9399  dffi3  9401  hartogslem1  9514  inf3lema  9603  inf3lemd  9606  cantnfle  9650  cantnflem2  9669  ttrclselem1  9704  trcl  9707  tcmin  9718  rankr1ai  9780  rankxplim  9861  scottex  9872  scottexOLD  9873  scott0b  9876  scott0OLD  9877  scottexsOLD  9882  scott0bsOLD  9884  scottelrankd  9887  kardenOLD  9899  cardne  9970  cardaleph  10092  ackbij2  10244  cflim2  10265  cfslb  10268  coftr  10275  fin23lem15  10336  fin23lem32  10346  fin23lem34  10348  fin23lem35  10349  fin23lem36  10350  fin23lem41  10354  isf32lem1  10355  itunitc1  10422  axdc3lem2  10453  ttukeylem1  10511  fpwwe2cbv  10633  fpwwe2lem2  10635  fpwwe2lem4  10637  fpwwe2  10646  fpwwecbv  10647  fpwwelem  10648  canthwelem  10653  canthwe  10654  pwfseqlem4  10665  wunex2  10741  wuncval2  10750  eltsk2g  10754  tskpwss  10755  inar1  10778  grothpw  10829  grothpwex  10830  axgroth6  10831  grothac  10833  peano5uzti  12704  fsuppmapnn0fiub0  14049  relexpnndm  15104  rtrclreclem4  15124  dfrtrcl2  15125  lo1o1  15609  o1lo1  15614  o1lo12  15615  lo1eq  15645  rlimeq  15646  isercoll  15745  prmreclem4  17004  vdwmc  17063  vdwlem1  17066  vdwlem2  17067  vdwlem12  17077  vdwlem13  17078  ramval  17093  ramz2  17109  ramub1lem1  17111  isacs2  17734  isacs1i  17738  mreacs  17739  acsfn  17740  rescabs  17915  ipole  18615  ipodrsima  18622  isacs5  18629  symgsssg  19568  psgnunilem5  19595  sylow1  19704  efgval2  19825  efgsfo  19840  frgpuplem  19873  gsumzf1o  20013  gsumzoppg  20045  dprdcntz  20111  islbs2  21315  frlmssuvc1  21981  frlmssuvc2  21982  frlmsslsp  21983  ismhp  22340  pptbas  23202  pnfnei  23414  mnfnei  23415  iscnp  23431  iscnp4  23457  cnntr  23469  cnconst2  23477  cnpresti  23482  cnprest  23483  isreg  23526  isnrm  23529  isnrm2  23552  perfcls  23559  isreg2  23571  hauscmplem  23600  1stcfb  23639  1stcelcls  23655  1stccnp  23656  txbas  23761  ptbasfi  23775  xkoopn  23783  xkoccn  23813  txcnp  23814  ptcnplem  23815  txdis  23826  txdis1cn  23829  txtube  23834  txkgen  23846  xkohaus  23847  xkoptsub  23848  xkoco1cn  23851  xkoco2cn  23852  xkococnlem  23853  xkococn  23854  xkoinjcn  23881  kqreglem1  23935  kqreglem2  23936  kqnrmlem1  23937  kqnrmlem2  23938  reghmph  23987  nrmhmph  23988  trfil2  24081  ufileu  24113  elfm  24141  elfm2  24142  elfm3  24144  imaelfm  24145  rnelfm  24147  fmfnfmlem2  24149  fmfnfmlem4  24151  fmco  24155  elflim2  24158  flffbas  24189  lmflf  24199  txflf  24200  fclscf  24219  flimfnfcls  24222  cnextcn  24261  symgtgp  24300  ghmcnp  24309  qustgplem  24315  eltsms  24327  ustval  24397  ust0  24414  trust  24423  utoptop  24428  restutop  24431  restutopopn  24432  utopsnneiplem  24441  ucncn  24478  fmucnd  24485  cfilufg  24486  trcfilu  24487  neipcfilu  24489  blssps  24618  blss  24619  ssblex  24622  blin2  24623  metss2  24706  metrest  24718  metcnp3  24734  metustexhalf  24750  metustbl  24760  psmetutop  24761  xrsmopn  25007  recld2  25009  icccmplem1  25017  icccmplem2  25018  icccmp  25020  reconnlem2  25022  lebnumlem3  25159  lebnum  25160  xlebnum  25161  lebnumii  25162  nmhmcn  25316  cfilfval  25460  caubl  25504  caublcls  25505  bcthlem1  25520  bcth  25525  ovolfiniun  25697  ovoliunlem3  25700  ovoliun  25701  ovoliun2  25702  ovoliunnul  25703  voliunlem3  25748  dyadmax  25794  dyadmbllem  25795  dyadmbl  25796  opnmbllem  25797  ellimc2  26073  limcnlp  26074  ellimc3  26075  limcflf  26077  limciun  26090  cpnord  26131  lhop  26212  xrlimcnp  27170  cvxcl  27186  dchrval  27435  noetalem2  27943  madebdayim  28118  madebdaylemold  28128  madebday  28130  bdayle  28146  precsexlem8  28444  bdaypw2n0bndlem  28693  bdayfinbndcbv  28696  bdayfinbndlem1  28697  bdayfinbndlem2  28698  bdayfinbnd  28699  lnssplng  29111  ausgrumgri  29554  ausgrusgri  29555  nbgrval  29723  nbgrel  29727  nbumgrvtx  29733  nbgrnself  29746  uvtxel1  29783  wlkonl1iedg  30050  crctcshwlkn0lem6  30201  2wlkdlem10  30321  1wlkdlem4  30528  3wlkdlem6  30553  3wlkdlem10  30557  eupth2lem3lem4  30619  frcond1  30654  frgr1v  30659  nfrgr2v  30660  frgr3vlem1  30661  frgr3vlem2  30662  frgr3v  30663  4cycl2vnunb  30678  n4cyclfrgr  30679  isssp  31113  ubthlem1  31259  shmodi  31779  chsupid  31801  chsscon3  31889  spansncvi  32041  mdslmd1lem3  32716  mdslmd1lem4  32717  mdsymlem5  32796  dmdbr5ati  32811  dmdbr6ati  32812  dmdbr7ati  32813  ssiun2sf  32941  fpwrelmapffslem  33114  prodindf  33219  pwrssmgc  33351  fldgenval  33664  unitprodclb  33733  esplysply  33992  esplyfvaln  33995  esplyind  33996  resssra  34008  constrsscn  34161  constrextdg2lem  34169  constrextdg2  34170  txomap  34255  locfinreflem  34261  tpr2rico  34333  pnfneige0  34372  rrhre  34442  dya2icoseg2  34700  omsfval  34716  eulerpartlemt0  34791  eulerpartgbij  34794  eulerpartlemr  34796  eulerpartlemgs2  34802  eulerpartlemn  34803  eulerpart  34804  bnj517  35305  bnj1014  35381  bnj1015  35382  bnj1123  35406  bnj1125  35412  bnj1450  35470  bnj1452  35472  elscott  35535  elkarden  35592  cplgredgex  35634  kur14  35729  cvmliftlem15  35811  cvmlift2lem12  35827  cvmlift2lem13  35828  mclsval  36076  mclsax  36082  mclsppslem  36096  prodeq12sdv  36771  cbvsumdavw2  36848  cbvproddavw2  36849  opnrebl  36872  opnrebl2  36873  ivthALT  36887  neibastop2lem  36912  fnemeet1  36918  filnetlem1  36930  filnetlem4  36933  ttcmin  37048  dfttc2g  37058  bj-imdirval3  37869  bj-imdiridlem  37870  rdgssun  38065  lindsadd  38305  lindsenlbs  38307  ptrecube  38312  poimirlem32  38344  opnmbllem0  38348  mblfinlem1  38349  mblfinlem2  38350  mblfinlem3  38351  ovoliunnfl  38354  ex-ovoliunnfl  38355  voliunnfl  38356  totbndbnd  38481  heibor1lem  38501  heiborlem10  38512  scottexf  38858  scott0f  38859  relcnveq2  39019  cnvref4  39040  dfcnvrefrels2  39298  dfcnvrefrel2  39300  elrelscnveq2  39319  symrefref2  39337  lcv1  39856  lfl1dim  39936  lfl1dim2N  39937  paddasslem17  40651  dihglblem6  42155  dochvalr  42172  dochord3  42187  lpolconN  42302  lcfls1lem  42349  mapdffval  42441  mapdfval  42442  mapdsn2  42457  mapd0  42480  lspindp5  42585  mapdh8ab  42592  primrootscoprbij  42910  aks6d1c2  42938  aks6d1c6lem3  42980  aks6d1c6lem5  42985  aks6d1c7lem1  42988  ismrcd1  43470  nacsfix  43484  setindtr  43792  hbtlem6  43897  oaabsb  44062  tfsconcatrnss  44118  naddwordnexlem4  44169  clcnvlem  44390  iunrelexpmin1  44475  iunrelexpmin2  44479  relexp0a  44483  cotrcltrcl  44492  trclimalb2  44493  cotrclrcl  44509  sbcheg  44546  clsk1indlem1  44812  isotone1  44815  isotone2  44816  ntrclsiso  44834  ntrclsk2  44835  k0004lem1  44914  k0004lem3  44916  mnuop123d  45013  mnuprdlem1  45023  mnuprdlem2  45024  mnuunid  45028  mnurndlem1  45032  modelaxreplem1  45728  modelaxreplem2  45729  modelaxrep  45731  ssdec  45847  iinssd  45890  iinssdf  45898  ssnnf1octb  45953  iooiinicc  46299  iooiinioc  46313  icccncfext  46642  fourierdlem41  46903  meaiininclem  47241  hoidmvlelem3  47352  hoidmvle  47355  opnvonmbllem1  47387  opnvonmbl  47389  iinhoiicclem  47428  smflim  47532  smflimsuplem7  47581  clnbgrval  48628  clnbgrel  48634  sclnbgrel  48653  isubgredg  48672  isubgruhgr  48674  uhgrimisgrgriclem  48736  uhgrimisgrgric  48737  clnbgrgrimlem  48739  clnbgrgrim  48740  isubgr3stgrlem7  48778  uspgrlimlem1  48794  uspgrlimlem2  48795  uspgrlimlem3  48796  uspgrlim  48798  pgnbgreunbgr  48931  uspgrsprf  48952  iinglb  49641  iscnrm3r  49767  iscnrm3l  49770  imassc  49972  setrecseq  50504  setrec1lem4  50509  setrec2fun  50511