Theorem sseq2d 3999

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  sseq12d  4000  sseqtrd  4007  sbcrel  5655  funimass2  6437  fnco  6465  fnssresb  6469  fnimaeq0  6481  foimacnv  6632  fvelimab  6737  ssimaexg  6749  knatar  7110  wfrdmcl  7963  wfrlem12  7966  onfununi  7978  oaordi  8172  oawordeulem  8180  oaass  8187  odi  8205  omass  8206  oen0  8212  oelim2  8221  nnaordi  8244  nnawordex  8263  pssnn  8736  fissuni  8829  dffi3  8895  cantnfle  9134  cantnflem1  9152  trcl  9170  r1sdom  9203  iscard2  9405  alephordi  9500  alephgeom  9508  cardaleph  9515  cardalephex  9516  ackbij2lem4  9664  cflm  9672  cfslbn  9689  cofsmo  9691  cfsmolem  9692  cfcoflem  9694  coftr  9695  alephsing  9698  fin23lem28  9762  fin23lem30  9764  fin23lem33  9767  fin1a2lem9  9830  axdc3lem2  9873  ttukeylem5  9935  fpwwe2lem5  10056  pwfseqlem4a  10083  pwfseqlem4  10084  wunex2  10160  inar1  10197  sstskm  10264  fsuppmapnn0fiubex  13361  swrdnd  14016  swrd0  14020  repswswrd  14146  rtrclreclem1  14417  rtrclreclem2  14418  summolem2  15073  summo  15074  zsum  15075  sumz  15079  sumss  15081  fsumcvg3  15086  prodmolem2  15289  prodmo  15290  zprod  15291  prod1  15298  vdwlem1  16317  vdwlem12  16328  vdwlem13  16329  ramub2  16350  rami  16351  ramz2  16360  setsstruct2  16521  prdsval  16728  pwsle  16765  mrcuni  16892  gsumpropd  17888  gsumpropd2lem  17889  gsumress  17892  eqgfval  18328  sscntz  18456  resscntz  18462  lsmlub  18790  efgrelexlemb  18876  efgcpbllemb  18881  gsumval3a  19023  gsumzaddlem  19041  gsumzoppg  19064  dmdprd  19120  dprdcntz  19130  subgdmdprd  19156  subrgpropd  19570  islss  19706  lsslss  19733  lsspropd  19789  lsmelpr  19863  lbspropd  19871  ltbval  20252  opsrval  20255  mhpval  20333  lsslinds  20975  isbasisg  21555  tgval  21563  tgss3  21594  restbas  21766  tgrest  21767  restcld  21780  restopn2  21785  restntr  21790  cnpnei  21872  cncls2  21881  perfcls  21973  cmpsublem  22007  cmpsub  22008  cmpcld  22010  uncmp  22011  hauscmplem  22014  cmpfi  22016  nconnsubb  22031  clsconn  22038  hausllycmp  22102  1stckgenlem  22161  txbas  22175  ptbasfi  22189  txcnpi  22216  ptcnp  22230  txcmplem1  22249  txcmplem2  22250  xkococnlem  22267  qtopcld  22321  fbasssin  22444  fbssint  22446  fbun  22448  fbasrn  22492  filufint  22528  ufinffr  22537  ufildr  22539  ustval  22811  trust  22838  elmopn  23052  neibl  23111  cfilucfil  23169  icccmplem1  23430  icccmplem2  23431  bndth  23562  isphtpc  23598  metcld  23909  bcthlem1  23927  bcth  23932  ovolfioo  24068  ovolficc  24069  elovolmr  24077  ovoliunlem3  24105  ovolicc2  24123  volsuplem  24156  dyadmax  24199  dyadmbllem  24200  dyadmbl  24201  incistruhgr  26864  edgssv2  26980  wksfval  27391  2wlkdlem9  27713  3wlkdlem9  27947  sspval  28500  ubth  28650  orthin  29223  chssoc  29273  chsscon3  29277  chsscon1  29278  h1datom  29359  pjoml6i  29366  osum  29422  spansncv  29430  pjcjt2  29469  pjopyth  29497  hstel2  29996  hstle  30007  stj  30012  dmdbr5  30085  mdslmd1lem1  30102  atord  30165  chirredlem4  30170  atcvat4i  30174  mdsymlem2  30181  mdsymlem3  30182  mdsymlem8  30187  padct  30455  ssnnssfz  30510  lindspropd  30943  tpr2rico  31155  ordtrestNEW  31164  sigaval  31370  issiga  31371  issgon  31382  oms0  31555  omssubadd  31558  subgrwlk  32379  umgr2cycllem  32387  kur14  32463  cvmliftlem15  32545  satfsschain  32611  mclsrcl  32808  mclsval  32810  trpredtr  33069  dftrpred3g  33072  frecseq123  33119  frrlem4  33126  ivthALT  33683  isfne  33687  topfne  33702  neibastop3  33710  tailfb  33725  filnetlem1  33726  filnetlem4  33729  csbwrecsg  34611  relowlssretop  34647  rdgssun  34662  poimirlem24  34931  mblfinlem2  34945  sstotbnd2  35067  sstotbnd  35068  sstotbnd3  35069  ssbnd  35081  cntotbnd  35089  cnpwstotbnd  35090  ismtyres  35101  heibor1lem  35102  heiborlem1  35104  heiborlem6  35109  heiborlem8  35111  exidreslem  35170  scottexf  35461  scott0f  35462  dfrefrels2  35768  dfrefrel2  35770  lshpcmp  36139  lsmsat  36159  lsmsatcv  36161  lfl1dim  36272  lfl1dim2N  36273  lkrss2N  36320  psubspset  36895  paddss  36996  psubclsetN  37087  dilfsetN  37303  dilsetN  37304  diaglbN  38206  dibglbN  38317  dihlspsnat  38484  dihglb2  38493  dochffval  38500  dochfval  38501  dochvalr  38508  dochord2N  38522  dochsncom  38533  dihjat1lem  38579  dvh4dimat  38589  dvh3dimatN  38590  dvh2dimatN  38591  dochexmidlem1  38611  lpolsetN  38633  lpolconN  38638  hdmaplkr  39064  hdmapoc  39082  hlhillcs  39109  ismrc  39347  incssnn0  39357  nacsfix  39358  hbt  39779  ss2iundf  40053  clsk1indlem1  40444  clsk1independent  40445  isotone1  40447  isotone2  40448  ntrclsiso  40466  ntrclsk2  40467  scottelrankd  40632  ssinc  41402  uzfissfz  41643  stoweidlem50  42384  stoweidlem57  42391  fourierdlem20  42461  fourierdlem50  42490  fourierdlem64  42504  fourierdlem86  42526  fourierdlem103  42543  fourierdlem104  42544  ovnval  42872  hoicvrrex  42887  ovnlecvr  42889  ovncvrrp  42895  ovnsubaddlem1  42901  hoidmvlelem3  42928  hoidmvle  42931  ovnhoilem1  42932  ovnhoi  42934  ovnlecvr2  42941  ovncvr2  42942  hspmbl  42960  ovolval4lem2  42981  ovolval5lem2  42984  ovolval5lem3  42985  ovolval5  42986  ovnovollem1  42987  ovnovollem2  42988  sprsymrelfvlem  43701  uspgrsprf  44070  uspgrsprfo  44072  ssnn0ssfz  44446  lincfsuppcl  44517