Theorem sseq2d 4014

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ⊆ wss 3948

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  sseq12d  4015  sseqtrd  4022  sbcrel  5779  funimass2  6629  fncoOLD  6666  fnssresb  6670  fnimaeq0  6681  foimacnv  6848  fvelimab  6962  ssimaexg  6975  knatar  7351  frecseq123  8264  frrlem4  8271  wfrdmclOLD  8314  wfrlem12OLD  8317  onfununi  8338  oaordi  8543  oawordeulem  8551  oaass  8558  odi  8576  omass  8577  oen0  8583  oelim2  8592  nnaordi  8615  nnawordex  8634  naddunif  8689  pssnn  9165  pssnnOLD  9262  fissuni  9354  dffi3  9423  cantnfle  9663  cantnflem1  9681  trcl  9720  r1sdom  9766  iscard2  9968  alephordi  10066  alephgeom  10074  cardaleph  10081  cardalephex  10082  ackbij2lem4  10234  cflm  10242  cfslbn  10259  cofsmo  10261  cfsmolem  10262  cfcoflem  10264  coftr  10265  alephsing  10268  fin23lem28  10332  fin23lem30  10334  fin23lem33  10337  fin1a2lem9  10400  axdc3lem2  10443  ttukeylem5  10505  fpwwe2lem4  10626  pwfseqlem4a  10653  pwfseqlem4  10654  wunex2  10730  inar1  10767  sstskm  10834  fsuppmapnn0fiubex  13954  swrdnd  14601  swrd0  14605  repswswrd  14731  rtrclreclem1  15001  rtrclreclem2  15003  summolem2  15659  summo  15660  zsum  15661  sumz  15665  sumss  15667  fsumcvg3  15672  prodmolem2  15876  prodmo  15877  zprod  15878  prod1  15885  vdwlem1  16911  vdwlem12  16922  vdwlem13  16923  ramub2  16944  rami  16945  ramz2  16954  setsstruct2  17104  prdsval  17398  pwsle  17435  mrcuni  17562  gsumpropd  18594  gsumpropd2lem  18595  gsumress  18598  eqgfval  19051  sscntz  19185  resscntz  19192  lsmlub  19527  efgrelexlemb  19613  efgcpbllemb  19618  gsumval3a  19766  gsumzaddlem  19784  gsumzoppg  19807  dmdprd  19863  dprdcntz  19873  subgdmdprd  19899  subrgpropd  20393  islss  20538  lsslss  20565  lsspropd  20621  lsmelpr  20695  lbspropd  20703  lsslinds  21378  ltbval  21590  opsrval  21593  mhpval  21675  isbasisg  22442  tgval  22450  tgss3  22481  restbas  22654  tgrest  22655  restcld  22668  restopn2  22673  restntr  22678  cnpnei  22760  cncls2  22769  perfcls  22861  cmpsublem  22895  cmpsub  22896  cmpcld  22898  uncmp  22899  hauscmplem  22902  cmpfi  22904  nconnsubb  22919  clsconn  22926  hausllycmp  22990  1stckgenlem  23049  txbas  23063  ptbasfi  23077  txcnpi  23104  ptcnp  23118  txcmplem1  23137  txcmplem2  23138  xkococnlem  23155  qtopcld  23209  fbasssin  23332  fbssint  23334  fbun  23336  fbasrn  23380  filufint  23416  ufinffr  23425  ufildr  23427  ustval  23699  trust  23726  elmopn  23940  neibl  24002  cfilucfil  24060  icccmplem1  24330  icccmplem2  24331  bndth  24466  isphtpc  24502  metcld  24815  bcthlem1  24833  bcth  24838  ovolfioo  24976  ovolficc  24977  elovolmr  24985  ovoliunlem3  25013  ovolicc2  25031  volsuplem  25064  dyadmax  25107  dyadmbllem  25108  dyadmbl  25109  precsexlem6  27648  precsexlem7  27649  incistruhgr  28329  edgssv2  28445  wksfval  28856  2wlkdlem9  29178  3wlkdlem9  29411  sspval  29964  ubth  30114  orthin  30687  chssoc  30737  chsscon3  30741  chsscon1  30742  h1datom  30823  pjoml6i  30830  osum  30886  spansncv  30894  pjcjt2  30933  pjopyth  30961  hstel2  31460  hstle  31471  stj  31476  dmdbr5  31549  mdslmd1lem1  31566  atord  31629  chirredlem4  31634  atcvat4i  31638  mdsymlem2  31645  mdsymlem3  31646  mdsymlem8  31651  padct  31932  ssnnssfz  31986  pwrssmgc  32158  lindspropd  32488  idlsrgval  32606  tpr2rico  32881  ordtrestNEW  32890  sigaval  33098  issiga  33099  issgon  33110  oms0  33285  omssubadd  33288  subgrwlk  34112  umgr2cycllem  34120  kur14  34196  cvmliftlem15  34278  satfsschain  34344  mclsrcl  34541  mclsval  34543  ivthALT  35209  isfne  35213  topfne  35228  neibastop3  35236  tailfb  35251  filnetlem1  35252  filnetlem4  35255  relowlssretop  36233  rdgssun  36248  poimirlem24  36501  mblfinlem2  36515  sstotbnd2  36631  sstotbnd  36632  sstotbnd3  36633  ssbnd  36645  cntotbnd  36653  cnpwstotbnd  36654  ismtyres  36665  heibor1lem  36666  heiborlem1  36668  heiborlem6  36673  heiborlem8  36675  exidreslem  36734  scottexf  37025  scott0f  37026  cnvref4  37208  dfrefrels2  37372  dfrefrel2  37374  lshpcmp  37847  lsmsat  37867  lsmsatcv  37869  lfl1dim  37980  lfl1dim2N  37981  lkrss2N  38028  psubspset  38604  paddss  38705  psubclsetN  38796  dilfsetN  39012  dilsetN  39013  diaglbN  39915  dibglbN  40026  dihlspsnat  40193  dihglb2  40202  dochffval  40209  dochfval  40210  dochvalr  40217  dochord2N  40231  dochsncom  40242  dihjat1lem  40288  dvh4dimat  40298  dvh3dimatN  40299  dvh2dimatN  40300  dochexmidlem1  40320  lpolsetN  40342  lpolconN  40347  hdmaplkr  40773  hdmapoc  40791  hlhillcs  40822  ismrc  41425  incssnn0  41435  nacsfix  41436  hbt  41858  oacl2g  42066  omcl2  42069  ofoaf  42091  naddwordnexlem4  42138  ss2iundf  42396  clsk1indlem1  42782  clsk1independent  42783  isotone1  42785  isotone2  42786  ntrclsiso  42804  ntrclsk2  42805  scottelrankd  42992  ssinc  43762  uzfissfz  44023  stoweidlem50  44753  stoweidlem57  44760  fourierdlem20  44830  fourierdlem50  44859  fourierdlem64  44873  fourierdlem86  44895  fourierdlem103  44912  fourierdlem104  44913  ovnval  45244  hoicvrrex  45259  ovnlecvr  45261  ovncvrrp  45267  ovnsubaddlem1  45273  hoidmvlelem3  45300  hoidmvle  45303  ovnhoilem1  45304  ovnhoi  45306  ovnlecvr2  45313  ovncvr2  45314  hspmbl  45332  ovolval4lem2  45353  ovolval5lem2  45356  ovolval5lem3  45357  ovolval5  45358  ovnovollem1  45359  ovnovollem2  45360  sprsymrelfvlem  46145  uspgrsprf  46511  uspgrsprfo  46513  subrngpropd  46732  ssnn0ssfz  46979  lincfsuppcl  47048  lubeldm2d  47545  glbeldm2d  47546