Theorem sseq2d 3940

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseq12d  3941  sseqtrd  3944  sbcrel  5756  funimass2  6623  fnssresb  6661  fnimaeq0  6672  foimacnv  6842  fvelimab  6957  ssimaexg  6971  ralima  7243  knatar  7367  frecseq123  8303  frrlem4  8310  onfununi  8352  oaordi  8557  oawordeulem  8565  oaass  8572  odi  8590  omass  8591  oen0  8598  oelim2  8607  nnaordi  8630  nnawordex  8649  naddunif  8706  pssnn  9187  fissuni  9349  dffi3  9426  cantnfle  9675  cantnflem1  9693  trcl  9732  r1sdom  9784  scottex  9936  scottelrankd  9951  iscard2  10060  alephordi  10156  alephgeom  10164  cardaleph  10171  cardalephex  10172  ackbij2lem4  10322  cflm  10330  cfslbn  10348  cofsmo  10350  cfsmolem  10351  cfcoflem  10353  coftr  10354  alephsing  10357  fin23lem28  10421  fin23lem30  10423  fin23lem33  10426  fin1a2lem9  10489  axdc3lem2  10532  ttukeylem5  10594  pwfseqlem4a  10749  pwfseqlem4  10750  wunex2  10826  inar1  10863  sstskm  10930  fsuppmapnn0fiubex  14138  swrdnd  14808  swrd0  14812  repswswrd  14939  rtrclreclem1  15215  rtrclreclem2  15217  summolem2  15887  summo  15888  zsum  15889  sumz  15893  sumss  15895  fsumcvg3  15900  prodmolem2  16107  prodmo  16108  zprod  16109  prod1  16116  vdwlem1  17164  vdwlem12  17175  vdwlem13  17176  ramub2  17197  rami  17198  ramz2  17207  setsstruct2  17357  prdsval  17631  pwsle  17669  mrcuni  17800  gsumpropd  18872  gsumpropd2lem  18873  gsumress  18876  eqgfval  19393  sscntz  19545  resscntz  19552  lsmlub  19883  efgrelexlemb  19969  efgcpbllemb  19974  gsumval3a  20122  gsumzaddlem  20140  gsumzoppg  20163  dmdprd  20219  dprdcntz  20229  subgdmdprd  20255  subrngpropd  20825  subrgpropd  20865  islss  21214  lsslss  21241  lsspropd  21297  lsmelpr  21371  lbspropd  21379  lsslinds  22142  ltbval  22357  opsrval  22360  mhpval  22465  isbasisg  23270  tgval  23278  tgss3  23309  restbas  23481  tgrest  23482  restcld  23495  restopn2  23500  restntr  23505  cnpnei  23587  cncls2  23596  perfcls  23688  cmpsublem  23722  cmpsub  23723  cmpcld  23725  uncmp  23726  hauscmplem  23729  cmpfi  23731  nconnsubb  23746  clsconn  23753  hausllycmp  23818  1stckgenlem  23877  txbas  23891  ptbasfi  23905  txcnpi  23932  ptcnp  23946  txcmplem1  23965  txcmplem2  23966  xkococnlem  23983  qtopcld  24037  fbasssin  24160  fbssint  24162  fbun  24164  fbasrn  24208  filufint  24244  ufinffr  24253  ufildr  24255  ustval  24527  trust  24553  elmopn  24766  neibl  24825  cfilucfil  24883  icccmplem1  25147  icccmplem2  25148  bndth  25284  isphtpc  25320  metcld  25632  bcthlem1  25650  bcth  25655  ovolfioo  25793  ovolficc  25794  elovolmr  25802  ovoliunlem3  25830  ovolicc2  25848  volsuplem  25881  dyadmax  25924  dyadmbllem  25925  dyadmbl  25926  precsexlem6  28603  precsexlem7  28604  bdayfinbndlem1  28858  bdayfinbndlem2  28859  lnssplng  29275  incistruhgr  29662  edgssv2  29784  wksfval  30195  subgrwlk  30274  2wlkdlem9  30528  3wlkdlem9  30774  sspval  31330  ubth  31480  orthin  32053  chssoc  32103  chsscon3  32107  chsscon1  32108  h1datom  32189  pjoml6i  32196  osum  32252  spansncv  32260  pjcjt2  32299  pjopyth  32327  hstel2  32826  hstle  32837  stj  32842  dmdbr5  32915  mdslmd1lem1  32932  atord  32995  chirredlem4  33000  atcvat4i  33004  mdsymlem2  33011  mdsymlem3  33012  mdsymlem8  33017  padct  33357  ssnnssfz  33425  pwrssmgc  33607  lindspropd  33984  idlsrgval  34081  constr01  34420  constrmon  34422  constrextdg2lem  34426  constrextdg2  34427  constrfiss  34429  tpr2rico  34590  ordtrestNEW  34599  sigaval  34789  issiga  34790  issgon  34801  oms0  34975  omssubadd  34978  elscottrankss  35801  acwer1prclem  35815  maxssj0  35945  onprcf1acwevdlem1  35964  kur14  36067  cvmliftlem15  36149  satfsschain  36215  mclsrcl  36412  mclsval  36414  nmulprop  37031  ivthALT  37215  isfne  37219  topfne  37234  neibastop3  37242  tailfb  37257  filnetlem1  37258  filnetlem4  37261  relowlssretop  38379  rdgssun  38394  poimirlem24  38655  mblfinlem2  38669  sstotbnd2  38801  sstotbnd  38802  sstotbnd3  38803  ssbnd  38815  cntotbnd  38823  cnpwstotbnd  38824  ismtyres  38835  heibor1lem  38836  heiborlem1  38838  heiborlem6  38843  heiborlem8  38845  exidreslem  38904  scottexf  39193  scott0f  39194  cnvref4  39375  dfrefrels2  39618  dfrefrel2  39620  lshpcmp  40138  lsmsat  40158  lsmsatcv  40160  lfl1dim  40271  lfl1dim2N  40272  lkrss2N  40319  psubspset  40894  paddss  40995  psubclsetN  41086  dilfsetN  41302  dilsetN  41303  diaglbN  42205  dibglbN  42316  dihlspsnat  42483  dihglb2  42492  dochffval  42499  dochfval  42500  dochvalr  42507  dochord2N  42521  dochsncom  42532  dihjat1lem  42578  dvh4dimat  42588  dvh3dimatN  42589  dvh2dimatN  42590  dochexmidlem1  42610  lpolsetN  42632  lpolconN  42637  hdmaplkr  43063  hdmapoc  43081  hlhillcs  43108  ismrc  43805  incssnn0  43815  nacsfix  43816  hbt  44225  oacl2g  44425  omcl2  44428  ofoaf  44450  naddwordnexlem4  44496  ss2iundf  44752  clsk1indlem1  45138  clsk1independent  45139  isotone1  45141  isotone2  45142  ntrclsiso  45160  ntrclsk2  45161  ssinc  46195  uzfissfz  46431  stoweidlem50  47153  stoweidlem57  47160  fourierdlem20  47230  fourierdlem50  47259  fourierdlem64  47273  fourierdlem86  47295  fourierdlem103  47312  fourierdlem104  47313  ovnval  47644  hoicvrrex  47659  ovnlecvr  47661  ovncvrrp  47667  ovnsubaddlem1  47673  hoidmvlelem3  47700  hoidmvle  47703  ovnhoilem1  47704  ovnhoi  47706  ovnlecvr2  47713  ovncvr2  47714  hspmbl  47732  ovolval4lem2  47753  ovolval5lem2  47756  ovolval5lem3  47757  ovolval5  47758  ovnovollem1  47759  ovnovollem2  47760  sprsymrelfvlem  48665  grlimedgclnbgr  49186  grlimgrtri  49194  grilcbri2  49202  uspgrsprf  49337  uspgrsprfo  49339  ssnn0ssfz  49554  lincfsuppcl  49618  iunlub  50025  lubeldm2d  50165  glbeldm2d  50166