Theorem sseq2d 3827

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

Hypothesis

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

Assertion

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

Proof of Theorem sseq2d

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1653   ⊆ wss 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781

This theorem is referenced by:  sseq12d  3828  sseqtrd  3835  sbcrel  5408  funimass2  6181  fnco  6208  fnssresb  6212  fnimaeq0  6222  foimacnv  6371  fvelimab  6476  ssimaexg  6487  knatar  6833  wfrdmcl  7660  wfrlem12  7663  onfununi  7675  oaordi  7864  oawordeulem  7872  oaass  7879  odi  7897  omass  7898  oen0  7904  oelim2  7913  nnaordi  7936  nnawordex  7955  pssnn  8418  fissuni  8511  dffi3  8577  cantnfle  8816  cantnflem1  8834  trcl  8852  r1sdom  8885  iscard2  9086  alephordi  9181  alephgeom  9189  cardaleph  9196  cardalephex  9197  ackbij2lem4  9350  cflm  9358  cfslbn  9375  cofsmo  9377  cfsmolem  9378  cfcoflem  9380  coftr  9381  alephsing  9384  fin23lem28  9448  fin23lem30  9450  fin23lem33  9453  fin1a2lem9  9516  axdc3lem2  9559  ttukeylem5  9621  fpwwe2lem5  9742  pwfseqlem4a  9769  pwfseqlem4  9770  wunex2  9846  inar1  9883  sstskm  9950  fsuppmapnn0fiubex  13042  swrdnd  13679  swrd0  13683  repswswrd  13860  rtrclreclem1  14135  rtrclreclem2  14136  summolem2  14784  summo  14785  zsum  14786  sumz  14790  sumss  14792  fsumcvg3  14797  prodmolem2  14998  prodmo  14999  zprod  15000  prod1  15007  vdwlem1  16014  vdwlem12  16025  vdwlem13  16026  ramub2  16047  rami  16048  ramz2  16057  setsstruct2  16218  prdsval  16426  pwsle  16463  mrcuni  16592  gsumpropd  17583  gsumpropd2lem  17584  gsumress  17587  eqgfval  17951  sscntz  18067  resscntz  18072  lsmlub  18387  efgrelexlemb  18474  efgcpbllemb  18479  gsumval3a  18615  gsumzaddlem  18632  gsumzoppg  18655  dmdprd  18709  dprdcntz  18719  subgdmdprd  18745  subrgpropd  19128  islss  19249  lsslss  19278  lsspropd  19334  lsmelpr  19408  lbspropd  19416  ltbval  19790  opsrval  19793  lsslinds  20491  isbasisg  21076  tgval  21084  tgss3  21115  restbas  21287  tgrest  21288  restcld  21301  restopn2  21306  restntr  21311  cnpnei  21393  cncls2  21402  perfcls  21494  cmpsublem  21527  cmpsub  21528  cmpcld  21530  uncmp  21531  hauscmplem  21534  cmpfi  21536  nconnsubb  21551  clsconn  21558  hausllycmp  21622  1stckgenlem  21681  txbas  21695  ptbasfi  21709  txcnpi  21736  ptcnp  21750  txcmplem1  21769  txcmplem2  21770  xkococnlem  21787  qtopcld  21841  fbasssin  21964  fbssint  21966  fbun  21968  fbasrn  22012  filufint  22048  ufinffr  22057  ufildr  22059  ustval  22330  trust  22357  elmopn  22571  neibl  22630  cfilucfil  22688  icccmplem1  22949  icccmplem2  22950  bndth  23081  isphtpc  23117  metcld  23428  bcthlem1  23446  bcth  23451  ovolfioo  23571  ovolficc  23572  elovolmr  23580  ovoliunlem3  23608  ovolicc2  23626  volsuplem  23659  dyadmax  23702  dyadmbllem  23703  dyadmbl  23704  incistruhgr  26305  edgssv2  26422  wksfval  26850  2wlkdlem9  27214  3wlkdlem9  27503  isfrgr  27598  sspval  28094  ubth  28245  orthin  28821  chssoc  28871  chsscon3  28875  chsscon1  28876  h1datom  28957  pjoml6i  28964  osum  29020  spansncv  29028  pjcjt2  29067  pjopyth  29095  hstel2  29594  hstle  29605  stj  29610  dmdbr5  29683  mdslmd1lem1  29700  atord  29763  chirredlem4  29768  atcvat4i  29772  mdsymlem2  29779  mdsymlem3  29780  mdsymlem8  29785  padct  30006  ssnnssfz  30058  tpr2rico  30465  ordtrestNEW  30474  sigaval  30680  issiga  30681  issgon  30693  oms0  30866  omssubadd  30869  kur14  31706  cvmliftlem15  31788  mclsrcl  31966  mclsval  31968  trpredtr  32233  dftrpred3g  32236  frecseq123  32281  frrlem4  32287  frrlem5e  32292  ivthALT  32833  isfne  32837  topfne  32852  neibastop3  32860  tailfb  32875  filnetlem1  32876  filnetlem4  32879  csbwrecsg  33663  relowlssretop  33700  poimirlem24  33913  mblfinlem2  33927  sstotbnd2  34051  sstotbnd  34052  sstotbnd3  34053  ssbnd  34065  cntotbnd  34073  cnpwstotbnd  34074  ismtyres  34085  heibor1lem  34086  heiborlem1  34088  heiborlem6  34093  heiborlem8  34095  exidreslem  34154  scottexf  34453  scott0f  34454  dfrefrels2  34748  dfrefrel2  34750  lshpcmp  35000  lsmsat  35020  lsmsatcv  35022  lfl1dim  35133  lfl1dim2N  35134  lkrss2N  35181  psubspset  35756  paddss  35857  psubclsetN  35948  dilfsetN  36164  dilsetN  36165  diaglbN  37067  dibglbN  37178  dihlspsnat  37345  dihglb2  37354  dochffval  37361  dochfval  37362  dochvalr  37369  dochord2N  37383  dochsncom  37394  dihjat1lem  37440  dvh4dimat  37450  dvh3dimatN  37451  dvh2dimatN  37452  dochexmidlem1  37472  lpolsetN  37494  lpolconN  37499  hdmaplkr  37925  hdmapoc  37943  hlhillcs  37970  ismrc  38037  incssnn0  38047  nacsfix  38048  hbt  38472  ss2iundf  38721  clsk1indlem1  39112  clsk1independent  39113  isotone1  39115  isotone2  39116  ntrclsiso  39134  ntrclsk2  39135  ssinc  40010  uzfissfz  40273  stoweidlem50  40997  stoweidlem57  41004  fourierdlem20  41074  fourierdlem50  41103  fourierdlem64  41117  fourierdlem86  41139  fourierdlem103  41156  fourierdlem104  41157  ovnval  41488  hoicvrrex  41503  ovnlecvr  41505  ovncvrrp  41511  ovnsubaddlem1  41517  hoidmvlelem3  41544  hoidmvle  41547  ovnhoilem1  41548  ovnhoi  41550  ovnlecvr2  41557  ovncvr2  41558  hspmbl  41576  ovolval4lem2  41597  ovolval5lem2  41600  ovolval5lem3  41601  ovolval5  41602  ovnovollem1  41603  ovnovollem2  41604  sprsymrelfvlem  42526  uspgrsprf  42540  uspgrsprfo  42542  ssnn0ssfz  42913  lincfsuppcl  42988