Theorem sseq2d 3954

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sseq12d  3955  sseqtrd  3962  sbcrel  5692  funimass2  6524  fncoOLD  6559  fnssresb  6563  fnimaeq0  6575  foimacnv  6742  fvelimab  6850  ssimaexg  6863  knatar  7237  frecseq123  8107  frrlem4  8114  wfrdmclOLD  8157  wfrlem12OLD  8160  onfununi  8181  oaordi  8386  oawordeulem  8394  oaass  8401  odi  8419  omass  8420  oen0  8426  oelim2  8435  nnaordi  8458  nnawordex  8477  pssnn  8960  pssnnOLD  9049  fissuni  9133  dffi3  9199  cantnfle  9438  cantnflem1  9456  trcl  9495  r1sdom  9541  iscard2  9743  alephordi  9839  alephgeom  9847  cardaleph  9854  cardalephex  9855  ackbij2lem4  10007  cflm  10015  cfslbn  10032  cofsmo  10034  cfsmolem  10035  cfcoflem  10037  coftr  10038  alephsing  10041  fin23lem28  10105  fin23lem30  10107  fin23lem33  10110  fin1a2lem9  10173  axdc3lem2  10216  ttukeylem5  10278  fpwwe2lem4  10399  pwfseqlem4a  10426  pwfseqlem4  10427  wunex2  10503  inar1  10540  sstskm  10607  fsuppmapnn0fiubex  13721  swrdnd  14376  swrd0  14380  repswswrd  14506  rtrclreclem1  14777  rtrclreclem2  14779  summolem2  15437  summo  15438  zsum  15439  sumz  15443  sumss  15445  fsumcvg3  15450  prodmolem2  15654  prodmo  15655  zprod  15656  prod1  15663  vdwlem1  16691  vdwlem12  16702  vdwlem13  16703  ramub2  16724  rami  16725  ramz2  16734  setsstruct2  16884  prdsval  17175  pwsle  17212  mrcuni  17339  gsumpropd  18371  gsumpropd2lem  18372  gsumress  18375  eqgfval  18813  sscntz  18941  resscntz  18947  lsmlub  19279  efgrelexlemb  19365  efgcpbllemb  19370  gsumval3a  19513  gsumzaddlem  19531  gsumzoppg  19554  dmdprd  19610  dprdcntz  19620  subgdmdprd  19646  subrgpropd  20068  islss  20205  lsslss  20232  lsspropd  20288  lsmelpr  20362  lbspropd  20370  lsslinds  21047  ltbval  21253  opsrval  21256  mhpval  21339  isbasisg  22106  tgval  22114  tgss3  22145  restbas  22318  tgrest  22319  restcld  22332  restopn2  22337  restntr  22342  cnpnei  22424  cncls2  22433  perfcls  22525  cmpsublem  22559  cmpsub  22560  cmpcld  22562  uncmp  22563  hauscmplem  22566  cmpfi  22568  nconnsubb  22583  clsconn  22590  hausllycmp  22654  1stckgenlem  22713  txbas  22727  ptbasfi  22741  txcnpi  22768  ptcnp  22782  txcmplem1  22801  txcmplem2  22802  xkococnlem  22819  qtopcld  22873  fbasssin  22996  fbssint  22998  fbun  23000  fbasrn  23044  filufint  23080  ufinffr  23089  ufildr  23091  ustval  23363  trust  23390  elmopn  23604  neibl  23666  cfilucfil  23724  icccmplem1  23994  icccmplem2  23995  bndth  24130  isphtpc  24166  metcld  24479  bcthlem1  24497  bcth  24502  ovolfioo  24640  ovolficc  24641  elovolmr  24649  ovoliunlem3  24677  ovolicc2  24695  volsuplem  24728  dyadmax  24771  dyadmbllem  24772  dyadmbl  24773  incistruhgr  27458  edgssv2  27574  wksfval  27985  2wlkdlem9  28308  3wlkdlem9  28541  sspval  29094  ubth  29244  orthin  29817  chssoc  29867  chsscon3  29871  chsscon1  29872  h1datom  29953  pjoml6i  29960  osum  30016  spansncv  30024  pjcjt2  30063  pjopyth  30091  hstel2  30590  hstle  30601  stj  30606  dmdbr5  30679  mdslmd1lem1  30696  atord  30759  chirredlem4  30764  atcvat4i  30768  mdsymlem2  30775  mdsymlem3  30776  mdsymlem8  30781  padct  31063  ssnnssfz  31117  pwrssmgc  31287  lindspropd  31586  idlsrgval  31657  tpr2rico  31871  ordtrestNEW  31880  sigaval  32088  issiga  32089  issgon  32100  oms0  32273  omssubadd  32276  subgrwlk  33103  umgr2cycllem  33111  kur14  33187  cvmliftlem15  33269  satfsschain  33335  mclsrcl  33532  mclsval  33534  ivthALT  34533  isfne  34537  topfne  34552  neibastop3  34560  tailfb  34575  filnetlem1  34576  filnetlem4  34579  relowlssretop  35543  rdgssun  35558  poimirlem24  35810  mblfinlem2  35824  sstotbnd2  35941  sstotbnd  35942  sstotbnd3  35943  ssbnd  35955  cntotbnd  35963  cnpwstotbnd  35964  ismtyres  35975  heibor1lem  35976  heiborlem1  35978  heiborlem6  35983  heiborlem8  35985  exidreslem  36044  scottexf  36335  scott0f  36336  dfrefrels2  36638  dfrefrel2  36640  lshpcmp  37009  lsmsat  37029  lsmsatcv  37031  lfl1dim  37142  lfl1dim2N  37143  lkrss2N  37190  psubspset  37765  paddss  37866  psubclsetN  37957  dilfsetN  38173  dilsetN  38174  diaglbN  39076  dibglbN  39187  dihlspsnat  39354  dihglb2  39363  dochffval  39370  dochfval  39371  dochvalr  39378  dochord2N  39392  dochsncom  39403  dihjat1lem  39449  dvh4dimat  39459  dvh3dimatN  39460  dvh2dimatN  39461  dochexmidlem1  39481  lpolsetN  39503  lpolconN  39508  hdmaplkr  39934  hdmapoc  39952  hlhillcs  39983  ismrc  40530  incssnn0  40540  nacsfix  40541  hbt  40962  ss2iundf  41274  clsk1indlem1  41662  clsk1independent  41663  isotone1  41665  isotone2  41666  ntrclsiso  41684  ntrclsk2  41685  scottelrankd  41872  ssinc  42644  uzfissfz  42872  stoweidlem50  43598  stoweidlem57  43605  fourierdlem20  43675  fourierdlem50  43704  fourierdlem64  43718  fourierdlem86  43740  fourierdlem103  43757  fourierdlem104  43758  ovnval  44086  hoicvrrex  44101  ovnlecvr  44103  ovncvrrp  44109  ovnsubaddlem1  44115  hoidmvlelem3  44142  hoidmvle  44145  ovnhoilem1  44146  ovnhoi  44148  ovnlecvr2  44155  ovncvr2  44156  hspmbl  44174  ovolval4lem2  44195  ovolval5lem2  44198  ovolval5lem3  44199  ovolval5  44200  ovnovollem1  44201  ovnovollem2  44202  sprsymrelfvlem  44953  uspgrsprf  45319  uspgrsprfo  45321  ssnn0ssfz  45696  lincfsuppcl  45765  lubeldm2d  46263  glbeldm2d  46264