Theorem eqsstrd 4021

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  eqsstrrd  4022  eqsstrdi  4037  fpr2g  7213  tfisi  7848  suppssof1  8184  suppss2  8185  onfununi  8341  oawordeulem  8554  oeeui  8602  nnawordex  8637  oaabslem  8646  oaabs2  8648  omabslem  8649  omabs  8650  cofonr  8673  pw2f1olem  9076  fodomr  9128  fival  9407  dffi3  9426  ordtypelem7  9519  ordtypelem8  9520  wemapso2lem  9547  cantnflt2  9668  cantnflem1  9684  tcss  9739  tcel  9740  r1val1  9781  rankuni2b  9848  tcrank  9879  cardonle  9952  harval2  9992  ackbij2  10238  cfub  10244  cflecard  10248  cfflb  10254  isf32lem8  10355  itunitc1  10415  ttukeylem7  10510  fpwwe2lem8  10633  wuncss  10740  wuncval2  10742  grur1a  10814  trclfvub  14954  cotrtrclfv  14959  relexpfld  14996  rtrclreclem4  15008  limsupgre  15425  isercolllem3  15613  4sqlem19  16896  vdwlem1  16914  vdwlem12  16925  ramub1lem1  16959  setsstruct2  17107  ressress  17193  imasaddfnlem  17474  imasaddflem  17476  imasvscafn  17483  imasvscaf  17485  imasless  17486  isohom  17723  ressffth  17889  acsfiindd  18506  acsmap2d  18508  dirref  18554  mndind  18709  f1omvdco2  19316  pmtrfrn  19326  symgsssg  19335  symggen  19338  psgnunilem1  19361  sylow2alem2  19486  lsmssv  19511  smndlsmidm  19524  gsumzres  19777  dprdlub  19896  dprdf1  19903  dprdsn  19906  dprdcntz2  19908  dprd2dlem1  19911  dprd2da  19912  dmdprdsplit2lem  19915  ablfac1eu  19943  drnglpir  20891  znleval  21110  evpmss  21139  frlmsplit2  21328  f1lindf  21377  issubassa2  21446  mplsubglem  21558  evlslem4  21637  evlseu  21646  mhpaddcl  21694  mhpinvcl  21695  lpsscls  22645  tgrest  22663  resttopon  22665  rest0  22673  restfpw  22683  ordtrest  22706  ordtrest2  22708  lmcnp  22808  tgcmp  22905  uncmp  22907  hauscmplem  22910  1stcfb  22949  2ndcdisj  22960  dissnref  23032  kgencmp  23049  xkouni  23103  prdstopn  23132  txtube  23144  txcmplem2  23146  xkoptsub  23158  xkopt  23159  xkococnlem  23163  qtoprest  23221  imastopn  23224  kqdisj  23236  reghmph  23297  nrmhmph  23298  fbssfi  23341  trfilss  23393  trfg  23395  elfm3  23454  alexsubALTlem3  23553  alexsubALT  23555  cnextf  23570  cnextcn  23571  clsnsg  23614  tgpconncompeqg  23616  qustgphaus  23627  trust  23734  ustuqtop3  23748  neipcfilu  23801  metequiv2  24019  prdsxmslem2  24038  metustfbas  24066  icccmplem1  24338  metdstri  24367  pi1addf  24563  pi1addval  24564  caubl  24825  caublcls  24826  relcmpcmet  24835  minveclem4  24949  hlhil  24960  ovolficcss  24986  uniioombllem3a  25101  uniioombllem3  25102  dyadss  25111  opnmbllem  25118  i1fima2  25196  limcfval  25389  dvfval  25414  dvnres  25448  dvivth  25527  lhop  25533  taylf  25873  xrlimcnp  26473  jensen  26493  ppisval  26608  chtlepsi  26709  chpub  26723  noextend  27169  nosupbday  27208  noinfbday  27223  scutun12  27312  scutbdaybnd  27317  scutbdaybnd2  27318  scutbdaylt  27320  cofcut1  27409  cofcutr  27413  negsbdaylem  27533  precsexlem8  27663  iscgrglt  27796  chssoc  30780  mdsl0  31594  mdexchi  31619  atcvat3i  31680  dmdbr5ati  31706  funimass4f  31892  xrofsup  32011  swrdrn2  32149  gsumpart  32238  pmtrcnel  32281  tocycfvres1  32300  tocycfvres2  32301  cycpmco2lem6  32321  cycpmconjvlem  32331  cycpmconjslem2  32345  fldgenssv  32436  fldgenssp  32439  nsgmgc  32554  idlsrgmulrss1  32656  idlsrgmulrss2  32657  fedgmullem1  32745  fedgmullem2  32746  ist0cld  32844  locfinreflem  32851  cmpcref  32861  zarcls0  32879  zarclsiin  32882  zarcmplem  32892  cnvordtrestixx  32924  ordtrestNEW  32932  ordtrest2NEW  32934  pnfneige0  32962  sigagenss  33178  imambfm  33292  dya2iocress  33304  dya2icoseg  33307  dya2iocucvr  33314  ballotlemro  33552  ftc2re  33641  bnj1097  34023  bnj1452  34094  cvmlift3lem6  34346  msubrn  34551  mclsssv  34586  mclsind  34592  liness  35148  neibastop2lem  35293  opnmbllem0  36572  mblfinlem2  36574  isbndx  36698  isbnd2  36699  ssbnd  36704  heiborlem3  36729  igenmin  36980  lsatlss  37914  lsmsat  37926  lsatfixedN  37927  lssats  37930  lpssat  37931  lssatle  37933  lssat  37934  lsatcvat3  37970  paddssat  38733  paddasslem17  38755  pmodlem2  38766  hlmod1i  38775  pl42lem4N  38901  diassdvaN  39979  dia2dimlem10  39992  cdlemn4a  40118  cdlemn5pre  40119  dihord5apre  40181  lclkrlem2e  40430  lclkrlem2p  40441  lclkrlem2v  40447  lclkrslem2  40457  lclkrs  40458  lcfrlem25  40486  lcfrlem35  40496  mapdval2N  40549  mapdpglem8  40598  mapdpglem13  40603  baerlem3lem2  40629  mapdindp2  40640  hdmap11lem2  40761  evlsmhpvvval  41215  prjspnssbas  41411  elrfi  41480  isnacs3  41496  mzpf  41522  mzpindd  41532  diophrw  41545  eldiophss  41560  rmxyelqirrOLD  41697  pw2f1ocnv  41824  aomclem6  41849  hbt  41920  rgspnmin  41961  oasubex  42084  oaabsb  42092  nnoeomeqom  42110  omcl2  42131  naddgeoa  42193  naddwordnexlem4  42200  oaltom  42204  omltoe  42206  minregex  42333  cnvssb  42385  trclubgNEW  42417  dfrcl2  42473  fvmptiunrelexplb0da  42484  relexp0a  42515  cotrcltrcl  42524  trclimalb2  42525  cotrclrcl  42541  isotone2  42848  k0004ss1  42950  fnresdmss  43912  mptelpm  43920  ssnnf1octb  43941  uzfissfz  44084  iuneqfzuzlem  44092  xlimliminflimsup  44626  icccncfext  44651  dvnprodlem1  44710  dvnprodlem2  44711  dvnprodlem3  44712  fourierdlem41  44912  fourierdlem70  44940  fourierdlem71  44941  fourierdlem80  44950  fourierdlem113  44983  ioorrnopnlem  45068  ioorrnopnxrlem  45070  salgenss  45100  dfsalgen2  45105  subsaliuncllem  45121  iundjiun  45224  meadjiunlem  45229  meaiunlelem  45232  meaiuninclem  45244  meaiininclem  45250  omeunle  45280  carageniuncllem2  45286  caratheodorylem1  45290  caratheodorylem2  45291  hoissre  45308  ovnsubaddlem1  45334  hoidmvlelem3  45361  ovnhoilem1  45365  ovnhoilem2  45366  ovnhoi  45367  ovncvr2  45375  voncmpl  45385  hspmbllem2  45391  hspmbl  45393  opnvonmbllem1  45396  vonmblss  45404  ovnsubadd2lem  45409  vonioolem2  45445  preimageiingt  45484  preimaleiinlt  45485  issmfd  45499  issmfdf  45501  sssmf  45502  cnfsmf  45504  issmfled  45521  issmfgtd  45525  smfadd  45529  smfrec  45553  smfmul  45559  smfmulc1  45560  smfpimbor1lem2  45563  smfsuplem1  45575  smflimsuplem1  45584  smflimsuplem7  45590  sprssspr  46197  linc1  47154