Theorem eqsstrd 3979

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 3976	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
4	1, 3	mpbird 260	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  eqsstrrd  3980  eqsstrdi  3989  3sstr4d  4000  fpr2g  7207  tfisi  7851  suppssof1  8191  suppss2  8192  onfununi  8324  oawordeulem  8535  oeeui  8584  nnawordex  8619  oaabslem  8629  oaabs2  8631  omabslem  8632  omabs  8633  cofonr  8656  pw2f1olem  9065  fodomr  9112  fodomfir  9283  fival  9368  dffi3  9387  ordtypelem7  9482  ordtypelem8  9483  wemapso2lem  9510  cantnflt2  9638  cantnflem1  9654  tcss  9707  tcel  9708  r1val1  9754  rankuni2b  9821  tcrank  9852  cardonle  9939  harval2  9979  ackbij2  10221  cfub  10228  cflecard  10232  cfflb  10239  isf32lem8  10340  itunitc1  10400  ttukeylem7  10495  fpwwe2lem8  10619  wuncss  10726  wuncval2  10728  grur1a  10800  trclfvub  15040  cotrtrclfv  15045  relexpfld  15082  rtrclreclem4  15094  limsupgre  15528  isercolllem3  15714  4sqlem19  17019  vdwlem1  17037  vdwlem12  17048  ramub1lem1  17082  setsstruct2  17230  ressress  17303  imasaddfnlem  17578  imasaddflem  17580  imasvscafn  17587  imasvscaf  17589  imasless  17590  isohom  17829  ressffth  17993  acsfiindd  18605  acsmap2d  18607  dirref  18653  mndind  18883  f1omvdco2  19514  pmtrfrn  19524  symgsssg  19533  symggen  19536  psgnunilem1  19559  sylow2alem2  19684  lsmssv  19709  smndlsmidm  19722  gsumzres  19975  dprdlub  20094  dprdf1  20101  dprdsn  20104  dprdcntz2  20106  dprd2dlem1  20109  dprd2da  20110  dmdprdsplit2lem  20113  ablfac1eu  20141  rgspnmin  20696  drnglpir  21465  znleval  21669  evpmss  21701  frlmsplit2  21888  f1lindf  21937  issubassa2  22007  mplsubglem  22113  evlslem4  22192  evlseu  22199  mhpaddcl  22279  mhpinvcl  22280  psdmul  22294  lpsscls  23263  tgrest  23281  resttopon  23283  rest0  23291  restfpw  23301  ordtrest  23324  ordtrest2  23326  lmcnp  23426  tgcmp  23523  uncmp  23525  hauscmplem  23528  1stcfb  23567  2ndcdisj  23578  dissnref  23650  kgencmp  23667  xkouni  23721  prdstopn  23750  txtube  23762  txcmplem2  23764  xkoptsub  23776  xkopt  23777  xkococnlem  23781  qtoprest  23839  imastopn  23842  kqdisj  23854  reghmph  23915  nrmhmph  23916  fbssfi  23959  trfilss  24011  trfg  24013  elfm3  24072  alexsubALTlem3  24171  alexsubALT  24173  cnextf  24188  cnextcn  24189  clsnsg  24232  tgpconncompeqg  24234  qustgphaus  24245  trust  24351  ustuqtop3  24365  neipcfilu  24417  metequiv2  24632  prdsxmslem2  24651  metustfbas  24679  icccmplem1  24945  metdstri  24974  pi1addf  25171  pi1addval  25172  caubl  25432  caublcls  25433  relcmpcmet  25442  minveclem4  25556  hlhil  25567  ovolficcss  25593  uniioombllem3a  25708  uniioombllem3  25709  dyadss  25718  opnmbllem  25725  i1fima2  25803  limcfval  25996  dvfval  26021  dvnres  26055  dvivth  26134  lhop  26140  taylf  26486  xrlimcnp  27095  jensen  27115  ppisval  27230  chtlepsi  27332  chpub  27346  noextend  27792  nosupbday  27831  noinfbday  27846  cutsun12  27945  cutbdaybnd  27950  cutbdaybnd2  27951  cutbdaylt  27953  sltsbday  28072  cofcut1  28075  cofcutr  28079  addbday  28173  negbdaylem  28211  precsexlem8  28369  bdayons  28431  onsbnd2  28437  noseqind  28447  n0bday  28507  bdaypw2n0bndlem  28618  iscgrglt  28745  cyclnumvtx  30086  chssoc  31785  mdsl0  32599  mdexchi  32624  atcvat3i  32685  dmdbr5ati  32711  funimass4f  32919  xrofsup  33049  swrdrn2  33211  gsumpart  33320  pmtrcnel  33346  tocycfvres1  33367  tocycfvres2  33368  cycpmco2lem6  33388  cycpmconjvlem  33398  cycpmconjslem2  33412  elrgspnsubrunlem2  33505  fldgenssv  33575  fldgenssp  33578  nsgmgc  33661  idlsrgmulrss1  33742  idlsrgmulrss2  33743  esplyfval1  33904  esplyfvaln  33905  esplyind  33906  fedgmullem1  33960  fedgmullem2  33961  constrsscn  34071  constrmon  34075  ist0cld  34164  locfinreflem  34171  cmpcref  34181  zarcls0  34199  zarclsiin  34202  zarcmplem  34212  cnvordtrestixx  34244  ordtrestNEW  34252  ordtrest2NEW  34254  pnfneige0  34282  sigagenss  34480  imambfm  34593  dya2iocress  34605  dya2icoseg  34608  dya2iocucvr  34615  ballotlemro  34854  ftc2re  34926  bnj1097  35310  bnj1452  35381  cvmlift3lem6  35711  msubrn  35916  mclsssv  35951  mclsind  35957  liness  36532  neibastop2lem  36756  ttcmin  36892  dfttc3gw  36919  opnmbllem0  38190  mblfinlem2  38192  isbndx  38316  isbnd2  38317  ssbnd  38322  heiborlem3  38347  igenmin  38598  lsatlss  39655  lsmsat  39667  lsatfixedN  39668  lssats  39671  lpssat  39672  lssatle  39674  lssat  39675  lsatcvat3  39711  paddssat  40473  paddasslem17  40495  pmodlem2  40506  hlmod1i  40515  pl42lem4N  40641  diassdvaN  41719  dia2dimlem10  41732  cdlemn4a  41858  cdlemn5pre  41859  dihord5apre  41921  lclkrlem2e  42170  lclkrlem2p  42181  lclkrlem2v  42187  lclkrslem2  42197  lclkrs  42198  lcfrlem25  42226  lcfrlem35  42236  mapdval2N  42289  mapdpglem8  42338  mapdpglem13  42343  baerlem3lem2  42369  mapdindp2  42380  hdmap11lem2  42501  primrootspoweq0  42758  aks6d1c6lem2  42823  evlsmhpvvval  43212  prjspnssbas  43238  elrfi  43310  isnacs3  43326  mzpf  43352  mzpindd  43362  diophrw  43375  eldiophss  43390  pw2f1ocnv  43649  aomclem6  43671  hbt  43742  oasubex  43898  oaabsb  43906  nnoeomeqom  43924  omcl2  43945  naddgeoa  44006  naddwordnexlem4  44013  oaltom  44016  omltoe  44018  minregex  44145  cnvssb  44197  trclubgNEW  44229  dfrcl2  44285  fvmptiunrelexplb0da  44296  relexp0a  44327  cotrcltrcl  44336  trclimalb2  44337  cotrclrcl  44353  isotone2  44660  k0004ss1  44762  fnresdmss  45771  mptelpm  45779  ssnnf1octb  45797  uzfissfz  45927  iuneqfzuzlem  45935  xlimliminflimsup  46461  icccncfext  46486  dvnprodlem2  46546  dvnprodlem3  46547  fourierdlem41  46747  fourierdlem70  46775  fourierdlem71  46776  fourierdlem80  46785  ioorrnopnlem  46903  ioorrnopnxrlem  46905  salgenss  46935  dfsalgen2  46940  subsaliuncllem  46956  iundjiun  47059  meadjiunlem  47064  meaiunlelem  47067  meaiuninclem  47079  meaiininclem  47085  omeunle  47115  carageniuncllem2  47121  caratheodorylem1  47125  caratheodorylem2  47126  hoissre  47143  ovnsubaddlem1  47169  hoidmvlelem3  47196  ovnhoilem1  47200  ovnhoilem2  47201  ovnhoi  47202  ovncvr2  47210  voncmpl  47220  hspmbllem2  47226  hspmbl  47228  opnvonmbllem1  47231  vonmblss  47239  ovnsubadd2lem  47244  vonioolem2  47280  preimaleiinlt  47320  issmfd  47334  issmfdf  47336  cnfsmf  47339  issmfled  47356  issmfgtd  47360  smfadd  47364  smfrec  47388  smfmul  47394  smfmulc1  47395  smfpimbor1lem2  47398  smfsuplem1  47410  smflimsuplem1  47419  smflimsuplem7  47425  sprssspr  48112  isubgredgss  48512  isubgrsubgr  48516  uhgrimisgrgriclem  48577  stgrnbgr0  48611  uspgrlimlem3  48637  linc1  49083  iinfssc  49713  discsubc  49720  idfullsubc  49817