Theorem sseq2d 3968

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sseq12d  3969  sseqtrd  3972  sbcrel  5751  funimass2  6600  fnssresb  6639  fnimaeq0  6650  foimacnv  6820  fvelimab  6935  ssimaexg  6949  ralima  7217  knatar  7337  frecseq123  8258  frrlem4  8265  onfununi  8307  oaordi  8510  oawordeulem  8518  oaass  8525  odi  8543  omass  8544  oen0  8551  oelim2  8560  nnaordi  8583  nnawordex  8602  naddunif  8659  pssnn  9133  fissuni  9297  dffi3  9374  cantnfle  9623  cantnflem1  9641  trcl  9680  r1sdom  9729  iscard2  9931  alephordi  10027  alephgeom  10035  cardaleph  10042  cardalephex  10043  ackbij2lem4  10194  cflm  10203  cfslbn  10221  cofsmo  10223  cfsmolem  10224  cfcoflem  10226  coftr  10227  alephsing  10230  fin23lem28  10294  fin23lem30  10296  fin23lem33  10299  fin1a2lem9  10362  axdc3lem2  10405  ttukeylem5  10467  pwfseqlem4a  10616  pwfseqlem4  10617  wunex2  10693  inar1  10730  sstskm  10797  fsuppmapnn0fiubex  14002  swrdnd  14665  swrd0  14669  repswswrd  14794  rtrclreclem1  15067  rtrclreclem2  15069  summolem2  15726  summo  15727  zsum  15728  sumz  15732  sumss  15734  fsumcvg3  15739  prodmolem2  15948  prodmo  15949  zprod  15950  prod1  15957  vdwlem1  17000  vdwlem12  17011  vdwlem13  17012  ramub2  17033  rami  17034  ramz2  17043  setsstruct2  17193  prdsval  17467  pwsle  17505  mrcuni  17636  gsumpropd  18695  gsumpropd2lem  18696  gsumress  18699  eqgfval  19200  sscntz  19349  resscntz  19356  lsmlub  19687  efgrelexlemb  19773  efgcpbllemb  19778  gsumval3a  19926  gsumzaddlem  19944  gsumzoppg  19967  dmdprd  20023  dprdcntz  20033  subgdmdprd  20059  subrngpropd  20597  subrgpropd  20637  islss  20981  lsslss  21008  lsspropd  21064  lsmelpr  21138  lbspropd  21146  lsslinds  21863  ltbval  22076  opsrval  22079  mhpval  22184  isbasisg  22987  tgval  22995  tgss3  23026  restbas  23198  tgrest  23199  restcld  23212  restopn2  23217  restntr  23222  cnpnei  23304  cncls2  23313  perfcls  23405  cmpsublem  23439  cmpsub  23440  cmpcld  23442  uncmp  23443  hauscmplem  23446  cmpfi  23448  nconnsubb  23463  clsconn  23470  hausllycmp  23534  1stckgenlem  23593  txbas  23607  ptbasfi  23621  txcnpi  23648  ptcnp  23662  txcmplem1  23681  txcmplem2  23682  xkococnlem  23699  qtopcld  23753  fbasssin  23876  fbssint  23878  fbun  23880  fbasrn  23924  filufint  23960  ufinffr  23969  ufildr  23971  ustval  24243  trust  24269  elmopn  24482  neibl  24541  cfilucfil  24599  icccmplem1  24863  icccmplem2  24864  bndth  25000  isphtpc  25036  metcld  25348  bcthlem1  25366  bcth  25371  ovolfioo  25509  ovolficc  25510  elovolmr  25518  ovoliunlem3  25546  ovolicc2  25564  volsuplem  25597  dyadmax  25640  dyadmbllem  25641  dyadmbl  25642  precsexlem6  28282  precsexlem7  28283  bdayfinbndlem1  28537  bdayfinbndlem2  28538  incistruhgr  29226  edgssv2  29345  wksfval  29756  2wlkdlem9  30080  3wlkdlem9  30316  sspval  30872  ubth  31022  orthin  31595  chssoc  31645  chsscon3  31649  chsscon1  31650  h1datom  31731  pjoml6i  31738  osum  31794  spansncv  31802  pjcjt2  31841  pjopyth  31869  hstel2  32368  hstle  32379  stj  32384  dmdbr5  32457  mdslmd1lem1  32474  atord  32537  chirredlem4  32542  atcvat4i  32546  mdsymlem2  32553  mdsymlem3  32554  mdsymlem8  32559  padct  32870  ssnnssfz  32939  pwrssmgc  33139  lindspropd  33530  idlsrgval  33660  constr01  34000  constrmon  34002  constrextdg2lem  34006  constrextdg2  34007  constrfiss  34009  tpr2rico  34170  ordtrestNEW  34179  sigaval  34369  issiga  34370  issgon  34381  oms0  34555  omssubadd  34558  subgrwlk  35446  umgr2cycllem  35454  kur14  35530  cvmliftlem15  35612  satfsschain  35678  mclsrcl  35875  mclsval  35877  nmulprop  36504  ivthALT  36659  isfne  36663  topfne  36678  neibastop3  36686  tailfb  36701  filnetlem1  36702  filnetlem4  36705  relowlssretop  37821  rdgssun  37836  poimirlem24  38107  mblfinlem2  38121  sstotbnd2  38237  sstotbnd  38238  sstotbnd3  38239  ssbnd  38251  cntotbnd  38259  cnpwstotbnd  38260  ismtyres  38271  heibor1lem  38272  heiborlem1  38274  heiborlem6  38279  heiborlem8  38281  exidreslem  38340  scottexf  38631  scott0f  38632  cnvref4  38813  dfrefrels2  39056  dfrefrel2  39058  lshpcmp  39576  lsmsat  39596  lsmsatcv  39598  lfl1dim  39709  lfl1dim2N  39710  lkrss2N  39757  psubspset  40332  paddss  40433  psubclsetN  40524  dilfsetN  40740  dilsetN  40741  diaglbN  41643  dibglbN  41754  dihlspsnat  41921  dihglb2  41930  dochffval  41937  dochfval  41938  dochvalr  41945  dochord2N  41959  dochsncom  41970  dihjat1lem  42016  dvh4dimat  42026  dvh3dimatN  42027  dvh2dimatN  42028  dochexmidlem1  42048  lpolsetN  42070  lpolconN  42075  hdmaplkr  42501  hdmapoc  42519  hlhillcs  42546  ismrc  43246  incssnn0  43256  nacsfix  43257  hbt  43671  oacl2g  43871  omcl2  43874  ofoaf  43896  naddwordnexlem4  43942  ss2iundf  44199  clsk1indlem1  44585  clsk1independent  44586  isotone1  44588  isotone2  44589  ntrclsiso  44607  ntrclsk2  44608  scottelrankd  44787  ssinc  45629  uzfissfz  45866  stoweidlem50  46588  stoweidlem57  46595  fourierdlem20  46665  fourierdlem50  46694  fourierdlem64  46708  fourierdlem86  46730  fourierdlem103  46747  fourierdlem104  46748  ovnval  47079  hoicvrrex  47094  ovnlecvr  47096  ovncvrrp  47102  ovnsubaddlem1  47108  hoidmvlelem3  47135  hoidmvle  47138  ovnhoilem1  47139  ovnhoi  47141  ovnlecvr2  47148  ovncvr2  47149  hspmbl  47167  ovolval4lem2  47188  ovolval5lem2  47191  ovolval5lem3  47192  ovolval5  47193  ovnovollem1  47194  ovnovollem2  47195  sprsymrelfvlem  48060  grlimedgclnbgr  48581  grlimgrtri  48589  grilcbri2  48597  uspgrsprf  48732  uspgrsprfo  48734  ssnn0ssfz  48935  lincfsuppcl  48999  iunlub  49406  lubeldm2d  49543  glbeldm2d  49544