Theorem eqsstrd 3968

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  eqsstrrd  3969  eqsstrdi  3978  3sstr4d  3989  fpr2g  7157  tfisi  7801  suppssof1  8141  suppss2  8142  onfununi  8273  oawordeulem  8481  oeeui  8530  nnawordex  8565  oaabslem  8575  oaabs2  8577  omabslem  8578  omabs  8579  cofonr  8602  pw2f1olem  9009  fodomr  9056  fodomfir  9228  fival  9315  dffi3  9334  ordtypelem7  9429  ordtypelem8  9430  wemapso2lem  9457  cantnflt2  9582  cantnflem1  9598  tcss  9651  tcel  9652  r1val1  9698  rankuni2b  9765  tcrank  9796  cardonle  9869  harval2  9909  ackbij2  10152  cfub  10159  cflecard  10163  cfflb  10169  isf32lem8  10270  itunitc1  10330  ttukeylem7  10425  fpwwe2lem8  10549  wuncss  10656  wuncval2  10658  grur1a  10730  trclfvub  14930  cotrtrclfv  14935  relexpfld  14972  rtrclreclem4  14984  limsupgre  15404  isercolllem3  15590  4sqlem19  16891  vdwlem1  16909  vdwlem12  16920  ramub1lem1  16954  setsstruct2  17101  ressress  17174  imasaddfnlem  17449  imasaddflem  17451  imasvscafn  17458  imasvscaf  17460  imasless  17461  isohom  17700  ressffth  17864  acsfiindd  18476  acsmap2d  18478  dirref  18524  mndind  18753  f1omvdco2  19377  pmtrfrn  19387  symgsssg  19396  symggen  19399  psgnunilem1  19422  sylow2alem2  19547  lsmssv  19572  smndlsmidm  19585  gsumzres  19838  dprdlub  19957  dprdf1  19964  dprdsn  19967  dprdcntz2  19969  dprd2dlem1  19972  dprd2da  19973  dmdprdsplit2lem  19976  ablfac1eu  20004  rgspnmin  20548  drnglpir  21287  znleval  21509  evpmss  21541  frlmsplit2  21728  f1lindf  21777  issubassa2  21848  mplsubglem  21954  evlslem4  22031  evlseu  22038  mhpaddcl  22094  mhpinvcl  22095  psdmul  22109  lpsscls  23085  tgrest  23103  resttopon  23105  rest0  23113  restfpw  23123  ordtrest  23146  ordtrest2  23148  lmcnp  23248  tgcmp  23345  uncmp  23347  hauscmplem  23350  1stcfb  23389  2ndcdisj  23400  dissnref  23472  kgencmp  23489  xkouni  23543  prdstopn  23572  txtube  23584  txcmplem2  23586  xkoptsub  23598  xkopt  23599  xkococnlem  23603  qtoprest  23661  imastopn  23664  kqdisj  23676  reghmph  23737  nrmhmph  23738  fbssfi  23781  trfilss  23833  trfg  23835  elfm3  23894  alexsubALTlem3  23993  alexsubALT  23995  cnextf  24010  cnextcn  24011  clsnsg  24054  tgpconncompeqg  24056  qustgphaus  24067  trust  24173  ustuqtop3  24187  neipcfilu  24239  metequiv2  24454  prdsxmslem2  24473  metustfbas  24501  icccmplem1  24767  metdstri  24796  pi1addf  25003  pi1addval  25004  caubl  25264  caublcls  25265  relcmpcmet  25274  minveclem4  25388  hlhil  25399  ovolficcss  25426  uniioombllem3a  25541  uniioombllem3  25542  dyadss  25551  opnmbllem  25558  i1fima2  25636  limcfval  25829  dvfval  25854  dvnres  25889  dvivth  25971  lhop  25977  taylf  26324  xrlimcnp  26934  jensen  26955  ppisval  27070  chtlepsi  27173  chpub  27187  noextend  27634  nosupbday  27673  noinfbday  27688  cutsun12  27786  cutbdaybnd  27791  cutbdaybnd2  27792  cutbdaylt  27794  sltsbday  27913  cofcut1  27916  cofcutr  27920  addbday  28014  negbdaylem  28052  precsexlem8  28210  bdayons  28272  onsbnd2  28278  noseqind  28288  n0bday  28348  bdaypw2n0bndlem  28459  iscgrglt  28586  cyclnumvtx  29873  chssoc  31571  mdsl0  32385  mdexchi  32410  atcvat3i  32471  dmdbr5ati  32497  funimass4f  32715  xrofsup  32847  swrdrn2  33036  gsumpart  33146  pmtrcnel  33171  tocycfvres1  33192  tocycfvres2  33193  cycpmco2lem6  33213  cycpmconjvlem  33223  cycpmconjslem2  33237  elrgspnsubrunlem2  33330  fldgenssv  33397  fldgenssp  33400  nsgmgc  33493  idlsrgmulrss1  33592  idlsrgmulrss2  33593  esplyind  33731  fedgmullem1  33786  fedgmullem2  33787  constrsscn  33897  constrmon  33901  ist0cld  33990  locfinreflem  33997  cmpcref  34007  zarcls0  34025  zarclsiin  34028  zarcmplem  34038  cnvordtrestixx  34070  ordtrestNEW  34078  ordtrest2NEW  34080  pnfneige0  34108  sigagenss  34306  imambfm  34419  dya2iocress  34431  dya2icoseg  34434  dya2iocucvr  34441  ballotlemro  34680  ftc2re  34755  bnj1097  35137  bnj1452  35208  cvmlift3lem6  35518  msubrn  35723  mclsssv  35758  mclsind  35764  liness  36339  neibastop2lem  36554  opnmbllem0  37857  mblfinlem2  37859  isbndx  37983  isbnd2  37984  ssbnd  37989  heiborlem3  38014  igenmin  38265  lsatlss  39256  lsmsat  39268  lsatfixedN  39269  lssats  39272  lpssat  39273  lssatle  39275  lssat  39276  lsatcvat3  39312  paddssat  40074  paddasslem17  40096  pmodlem2  40107  hlmod1i  40116  pl42lem4N  40242  diassdvaN  41320  dia2dimlem10  41333  cdlemn4a  41459  cdlemn5pre  41460  dihord5apre  41522  lclkrlem2e  41771  lclkrlem2p  41782  lclkrlem2v  41788  lclkrslem2  41798  lclkrs  41799  lcfrlem25  41827  lcfrlem35  41837  mapdval2N  41890  mapdpglem8  41939  mapdpglem13  41944  baerlem3lem2  41970  mapdindp2  41981  hdmap11lem2  42102  primrootspoweq0  42360  aks6d1c6lem2  42425  evlsmhpvvval  42838  prjspnssbas  42864  elrfi  42936  isnacs3  42952  mzpf  42978  mzpindd  42988  diophrw  43001  eldiophss  43016  pw2f1ocnv  43279  aomclem6  43301  hbt  43372  oasubex  43528  oaabsb  43536  nnoeomeqom  43554  omcl2  43575  naddgeoa  43636  naddwordnexlem4  43643  oaltom  43646  omltoe  43648  minregex  43775  cnvssb  43827  trclubgNEW  43859  dfrcl2  43915  fvmptiunrelexplb0da  43926  relexp0a  43957  cotrcltrcl  43966  trclimalb2  43967  cotrclrcl  43983  isotone2  44290  k0004ss1  44392  fnresdmss  45412  mptelpm  45420  ssnnf1octb  45438  uzfissfz  45571  iuneqfzuzlem  45579  xlimliminflimsup  46106  icccncfext  46131  dvnprodlem2  46191  dvnprodlem3  46192  fourierdlem41  46392  fourierdlem70  46420  fourierdlem71  46421  fourierdlem80  46430  fourierdlem113  46463  ioorrnopnlem  46548  ioorrnopnxrlem  46550  salgenss  46580  dfsalgen2  46585  subsaliuncllem  46601  iundjiun  46704  meadjiunlem  46709  meaiunlelem  46712  meaiuninclem  46724  meaiininclem  46730  omeunle  46760  carageniuncllem2  46766  caratheodorylem1  46770  caratheodorylem2  46771  hoissre  46788  ovnsubaddlem1  46814  hoidmvlelem3  46841  ovnhoilem1  46845  ovnhoilem2  46846  ovnhoi  46847  ovncvr2  46855  voncmpl  46865  hspmbllem2  46871  hspmbl  46873  opnvonmbllem1  46876  vonmblss  46884  ovnsubadd2lem  46889  vonioolem2  46925  preimaleiinlt  46965  issmfd  46979  issmfdf  46981  sssmf  46982  cnfsmf  46984  issmfled  47001  issmfgtd  47005  smfadd  47009  smfrec  47033  smfmul  47039  smfmulc1  47040  smfpimbor1lem2  47043  smfsuplem1  47055  smflimsuplem1  47064  smflimsuplem7  47070  sprssspr  47727  isubgredgss  48111  isubgrsubgr  48115  uhgrimisgrgriclem  48176  stgrnbgr0  48210  uspgrlimlem3  48236  linc1  48671  iinfssc  49302  discsubc  49309  idfullsubc  49406