Theorem sseq2d 3949

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sseq12d  3950  sseqtrd  3957  sbcrel  5681  funimass2  6501  fncoOLD  6534  fnssresb  6538  fnimaeq0  6550  foimacnv  6717  fvelimab  6823  ssimaexg  6836  knatar  7208  frecseq123  8069  frrlem4  8076  wfrdmclOLD  8119  wfrlem12OLD  8122  onfununi  8143  oaordi  8339  oawordeulem  8347  oaass  8354  odi  8372  omass  8373  oen0  8379  oelim2  8388  nnaordi  8411  nnawordex  8430  pssnn  8913  pssnnOLD  8969  fissuni  9054  dffi3  9120  cantnfle  9359  cantnflem1  9377  trpredtr  9408  dftrpred3g  9412  trcl  9417  r1sdom  9463  iscard2  9665  alephordi  9761  alephgeom  9769  cardaleph  9776  cardalephex  9777  ackbij2lem4  9929  cflm  9937  cfslbn  9954  cofsmo  9956  cfsmolem  9957  cfcoflem  9959  coftr  9960  alephsing  9963  fin23lem28  10027  fin23lem30  10029  fin23lem33  10032  fin1a2lem9  10095  axdc3lem2  10138  ttukeylem5  10200  fpwwe2lem4  10321  pwfseqlem4a  10348  pwfseqlem4  10349  wunex2  10425  inar1  10462  sstskm  10529  fsuppmapnn0fiubex  13640  swrdnd  14295  swrd0  14299  repswswrd  14425  rtrclreclem1  14696  rtrclreclem2  14698  summolem2  15356  summo  15357  zsum  15358  sumz  15362  sumss  15364  fsumcvg3  15369  prodmolem2  15573  prodmo  15574  zprod  15575  prod1  15582  vdwlem1  16610  vdwlem12  16621  vdwlem13  16622  ramub2  16643  rami  16644  ramz2  16653  setsstruct2  16803  prdsval  17083  pwsle  17120  mrcuni  17247  gsumpropd  18277  gsumpropd2lem  18278  gsumress  18281  eqgfval  18719  sscntz  18847  resscntz  18853  lsmlub  19185  efgrelexlemb  19271  efgcpbllemb  19276  gsumval3a  19419  gsumzaddlem  19437  gsumzoppg  19460  dmdprd  19516  dprdcntz  19526  subgdmdprd  19552  subrgpropd  19974  islss  20111  lsslss  20138  lsspropd  20194  lsmelpr  20268  lbspropd  20276  lsslinds  20948  ltbval  21154  opsrval  21157  mhpval  21240  isbasisg  22005  tgval  22013  tgss3  22044  restbas  22217  tgrest  22218  restcld  22231  restopn2  22236  restntr  22241  cnpnei  22323  cncls2  22332  perfcls  22424  cmpsublem  22458  cmpsub  22459  cmpcld  22461  uncmp  22462  hauscmplem  22465  cmpfi  22467  nconnsubb  22482  clsconn  22489  hausllycmp  22553  1stckgenlem  22612  txbas  22626  ptbasfi  22640  txcnpi  22667  ptcnp  22681  txcmplem1  22700  txcmplem2  22701  xkococnlem  22718  qtopcld  22772  fbasssin  22895  fbssint  22897  fbun  22899  fbasrn  22943  filufint  22979  ufinffr  22988  ufildr  22990  ustval  23262  trust  23289  elmopn  23503  neibl  23563  cfilucfil  23621  icccmplem1  23891  icccmplem2  23892  bndth  24027  isphtpc  24063  metcld  24375  bcthlem1  24393  bcth  24398  ovolfioo  24536  ovolficc  24537  elovolmr  24545  ovoliunlem3  24573  ovolicc2  24591  volsuplem  24624  dyadmax  24667  dyadmbllem  24668  dyadmbl  24669  incistruhgr  27352  edgssv2  27468  wksfval  27879  2wlkdlem9  28200  3wlkdlem9  28433  sspval  28986  ubth  29136  orthin  29709  chssoc  29759  chsscon3  29763  chsscon1  29764  h1datom  29845  pjoml6i  29852  osum  29908  spansncv  29916  pjcjt2  29955  pjopyth  29983  hstel2  30482  hstle  30493  stj  30498  dmdbr5  30571  mdslmd1lem1  30588  atord  30651  chirredlem4  30656  atcvat4i  30660  mdsymlem2  30667  mdsymlem3  30668  mdsymlem8  30673  padct  30956  ssnnssfz  31010  pwrssmgc  31180  lindspropd  31479  idlsrgval  31550  tpr2rico  31764  ordtrestNEW  31773  sigaval  31979  issiga  31980  issgon  31991  oms0  32164  omssubadd  32167  subgrwlk  32994  umgr2cycllem  33002  kur14  33078  cvmliftlem15  33160  satfsschain  33226  mclsrcl  33423  mclsval  33425  ivthALT  34451  isfne  34455  topfne  34470  neibastop3  34478  tailfb  34493  filnetlem1  34494  filnetlem4  34497  relowlssretop  35461  rdgssun  35476  poimirlem24  35728  mblfinlem2  35742  sstotbnd2  35859  sstotbnd  35860  sstotbnd3  35861  ssbnd  35873  cntotbnd  35881  cnpwstotbnd  35882  ismtyres  35893  heibor1lem  35894  heiborlem1  35896  heiborlem6  35901  heiborlem8  35903  exidreslem  35962  scottexf  36253  scott0f  36254  dfrefrels2  36558  dfrefrel2  36560  lshpcmp  36929  lsmsat  36949  lsmsatcv  36951  lfl1dim  37062  lfl1dim2N  37063  lkrss2N  37110  psubspset  37685  paddss  37786  psubclsetN  37877  dilfsetN  38093  dilsetN  38094  diaglbN  38996  dibglbN  39107  dihlspsnat  39274  dihglb2  39283  dochffval  39290  dochfval  39291  dochvalr  39298  dochord2N  39312  dochsncom  39323  dihjat1lem  39369  dvh4dimat  39379  dvh3dimatN  39380  dvh2dimatN  39381  dochexmidlem1  39401  lpolsetN  39423  lpolconN  39428  hdmaplkr  39854  hdmapoc  39872  hlhillcs  39903  ismrc  40439  incssnn0  40449  nacsfix  40450  hbt  40871  ss2iundf  41156  clsk1indlem1  41544  clsk1independent  41545  isotone1  41547  isotone2  41548  ntrclsiso  41566  ntrclsk2  41567  scottelrankd  41754  ssinc  42526  uzfissfz  42755  stoweidlem50  43481  stoweidlem57  43488  fourierdlem20  43558  fourierdlem50  43587  fourierdlem64  43601  fourierdlem86  43623  fourierdlem103  43640  fourierdlem104  43641  ovnval  43969  hoicvrrex  43984  ovnlecvr  43986  ovncvrrp  43992  ovnsubaddlem1  43998  hoidmvlelem3  44025  hoidmvle  44028  ovnhoilem1  44029  ovnhoi  44031  ovnlecvr2  44038  ovncvr2  44039  hspmbl  44057  ovolval4lem2  44078  ovolval5lem2  44081  ovolval5lem3  44082  ovolval5  44083  ovnovollem1  44084  ovnovollem2  44085  sprsymrelfvlem  44830  uspgrsprf  45196  uspgrsprfo  45198  ssnn0ssfz  45573  lincfsuppcl  45642  lubeldm2d  46140  glbeldm2d  46141