Theorem eqsstrd 3972

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqsstrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrd

Step	Hyp	Ref	Expression
1		eqsstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		eqsstrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	sseq1d 3969	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
4	1, 3	mpbird 260	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  eqsstrrd  3973  eqsstrdi  3982  3sstr4d  3993  fpr2g  7211  tfisi  7856  suppssof1  8196  suppss2  8197  onfununi  8329  oawordeulem  8540  oeeui  8589  nnawordex  8624  oaabslem  8634  oaabs2  8636  omabslem  8637  omabs  8638  cofonr  8661  pw2f1olem  9070  fodomr  9117  fodomfir  9288  fival  9373  dffi3  9392  ordtypelem7  9487  ordtypelem8  9488  wemapso2lem  9515  cantnflt2  9643  cantnflem1  9659  tcss  9712  tcel  9713  r1val1  9759  rankuni2b  9826  tcrank  9857  cardonle  9944  harval2  9984  ackbij2  10226  cfub  10233  cflecard  10237  cfflb  10244  isf32lem8  10345  itunitc1  10405  ttukeylem7  10500  fpwwe2lem8  10624  wuncss  10731  wuncval2  10733  grur1a  10805  trclfvub  15046  cotrtrclfv  15051  relexpfld  15088  rtrclreclem4  15100  limsupgre  15534  isercolllem3  15720  4sqlem19  17024  vdwlem1  17042  vdwlem12  17053  ramub1lem1  17087  setsstruct2  17235  ressress  17308  imasaddfnlem  17583  imasaddflem  17585  imasvscafn  17592  imasvscaf  17594  imasless  17595  isohom  17834  ressffth  17998  acsfiindd  18610  acsmap2d  18612  dirref  18658  mndind  18888  f1omvdco2  19519  pmtrfrn  19529  symgsssg  19538  symggen  19541  psgnunilem1  19564  sylow2alem2  19689  lsmssv  19714  smndlsmidm  19727  gsumzres  19980  dprdlub  20099  dprdf1  20106  dprdsn  20109  dprdcntz2  20111  dprd2dlem1  20114  dprd2da  20115  dmdprdsplit2lem  20118  ablfac1eu  20146  rgspnmin  20701  drnglpir  21481  znleval  21685  evpmss  21717  frlmsplit2  21904  f1lindf  21953  issubassa2  22023  mplsubglem  22129  evlslem4  22208  evlseu  22215  mhpaddcl  22295  mhpinvcl  22296  psdmul  22310  lpsscls  23279  tgrest  23297  resttopon  23299  rest0  23307  restfpw  23317  ordtrest  23340  ordtrest2  23342  lmcnp  23442  tgcmp  23539  uncmp  23541  hauscmplem  23544  1stcfb  23583  2ndcdisj  23594  dissnref  23666  kgencmp  23683  xkouni  23737  prdstopn  23766  txtube  23778  txcmplem2  23780  xkoptsub  23792  xkopt  23793  xkococnlem  23797  qtoprest  23855  imastopn  23858  kqdisj  23870  reghmph  23931  nrmhmph  23932  fbssfi  23975  trfilss  24027  trfg  24029  elfm3  24088  alexsubALTlem3  24187  alexsubALT  24189  cnextf  24204  cnextcn  24205  clsnsg  24248  tgpconncompeqg  24250  qustgphaus  24261  trust  24367  ustuqtop3  24381  neipcfilu  24433  metequiv2  24648  prdsxmslem2  24667  metustfbas  24695  icccmplem1  24961  metdstri  24990  pi1addf  25187  pi1addval  25188  caubl  25448  caublcls  25449  relcmpcmet  25458  minveclem4  25572  hlhil  25583  ovolficcss  25609  uniioombllem3a  25724  uniioombllem3  25725  dyadss  25734  opnmbllem  25741  i1fima2  25819  limcfval  26012  dvfval  26037  dvnres  26071  dvivth  26150  lhop  26156  taylf  26505  xrlimcnp  27114  jensen  27134  ppisval  27249  chtlepsi  27351  chpub  27365  noextend  27811  nosupbday  27850  noinfbday  27865  cutsun12  27964  cutbdaybnd  27969  cutbdaybnd2  27970  cutbdaylt  27972  sltsbday  28091  cofcut1  28094  cofcutr  28098  addbday  28192  negbdaylem  28230  precsexlem8  28388  bdayons  28450  onsbnd2  28456  noseqind  28466  n0bday  28526  bdaypw2n0bndlem  28637  iscgrglt  28764  cyclnumvtx  30130  chssoc  31829  mdsl0  32643  mdexchi  32668  atcvat3i  32729  dmdbr5ati  32755  funimass4f  32963  xrofsup  33093  swrdrn2  33255  gsumpart  33364  pmtrcnel  33390  tocycfvres1  33411  tocycfvres2  33412  cycpmco2lem6  33432  cycpmconjvlem  33442  cycpmconjslem2  33456  elrgspnsubrunlem2  33549  fldgenssv  33617  fldgenssp  33620  nsgmgc  33702  idlsrgmulrss1  33782  idlsrgmulrss2  33783  esplyfval1  33944  esplyfvaln  33945  esplyind  33946  fedgmullem1  34000  fedgmullem2  34001  constrsscn  34111  constrmon  34115  ist0cld  34204  locfinreflem  34211  cmpcref  34221  zarcls0  34239  zarclsiin  34242  zarcmplem  34252  cnvordtrestixx  34284  ordtrestNEW  34292  ordtrest2NEW  34294  pnfneige0  34322  sigagenss  34520  imambfm  34633  dya2iocress  34645  dya2icoseg  34648  dya2iocucvr  34655  ballotlemro  34894  ftc2re  34966  bnj1097  35350  bnj1452  35421  rankscottu  35504  cvmlift3lem6  35797  msubrn  36002  mclsssv  36037  mclsind  36043  liness  36618  neibastop2lem  36852  ttcmin  36988  dfttc3gw  37015  opnmbllem0  38288  mblfinlem2  38290  isbndx  38414  isbnd2  38415  ssbnd  38420  heiborlem3  38445  igenmin  38696  lsatlss  39751  lsmsat  39763  lsatfixedN  39764  lssats  39767  lpssat  39768  lssatle  39770  lssat  39771  lsatcvat3  39807  paddssat  40569  paddasslem17  40591  pmodlem2  40602  hlmod1i  40611  pl42lem4N  40737  diassdvaN  41815  dia2dimlem10  41828  cdlemn4a  41954  cdlemn5pre  41955  dihord5apre  42017  lclkrlem2e  42266  lclkrlem2p  42277  lclkrlem2v  42283  lclkrslem2  42293  lclkrs  42294  lcfrlem25  42322  lcfrlem35  42332  mapdval2N  42385  mapdpglem8  42434  mapdpglem13  42439  baerlem3lem2  42465  mapdindp2  42476  hdmap11lem2  42597  primrootspoweq0  42854  aks6d1c6lem2  42919  evlsmhpvvval  43310  prjspnssbas  43336  elrfi  43408  isnacs3  43424  mzpf  43450  mzpindd  43460  diophrw  43473  eldiophss  43488  pw2f1ocnv  43747  aomclem6  43769  hbt  43840  oasubex  43996  oaabsb  44004  nnoeomeqom  44022  omcl2  44043  naddgeoa  44104  naddwordnexlem4  44111  oaltom  44114  omltoe  44116  minregex  44243  cnvssb  44295  trclubgNEW  44327  dfrcl2  44383  fvmptiunrelexplb0da  44394  relexp0a  44425  cotrcltrcl  44434  trclimalb2  44435  cotrclrcl  44451  isotone2  44758  k0004ss1  44860  fnresdmss  45869  mptelpm  45877  ssnnf1octb  45895  uzfissfz  46025  iuneqfzuzlem  46033  xlimliminflimsup  46559  icccncfext  46584  dvnprodlem2  46644  dvnprodlem3  46645  fourierdlem41  46845  fourierdlem70  46873  fourierdlem71  46874  fourierdlem80  46883  ioorrnopnlem  47001  ioorrnopnxrlem  47003  salgenss  47033  dfsalgen2  47038  subsaliuncllem  47054  iundjiun  47157  meadjiunlem  47162  meaiunlelem  47165  meaiuninclem  47177  meaiininclem  47183  omeunle  47213  carageniuncllem2  47219  caratheodorylem1  47223  caratheodorylem2  47224  hoissre  47241  ovnsubaddlem1  47267  hoidmvlelem3  47294  ovnhoilem1  47298  ovnhoilem2  47299  ovnhoi  47300  ovncvr2  47308  voncmpl  47318  hspmbllem2  47324  hspmbl  47326  opnvonmbllem1  47329  vonmblss  47337  ovnsubadd2lem  47342  vonioolem2  47378  preimaleiinlt  47418  issmfd  47432  issmfdf  47434  cnfsmf  47437  issmfled  47454  issmfgtd  47458  smfadd  47462  smfrec  47486  smfmul  47492  smfmulc1  47493  smfpimbor1lem2  47496  smfsuplem1  47508  smflimsuplem1  47517  smflimsuplem7  47523  sprssspr  48213  isubgredgss  48613  isubgrsubgr  48617  uhgrimisgrgriclem  48678  stgrnbgr0  48712  uspgrlimlem3  48738  linc1  49188  iinfssc  49818  discsubc  49825  idfullsubc  49922