Theorem eqsstrd 3925

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

Syntax hints:   → wi 4   = wceq 1543   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  eqsstrrd  3926  eqsstrdi  3941  fpr2g  7005  tfisi  7615  suppssof1  7919  suppss2  7920  onfununi  8056  oawordeulem  8260  oeeui  8308  nnawordex  8343  oaabslem  8350  oaabs2  8352  omabslem  8353  omabs  8354  pw2f1olem  8727  fodomr  8775  fival  9006  dffi3  9025  ordtypelem7  9118  ordtypelem8  9119  wemapso2lem  9146  cantnflt2  9266  cantnflem1  9282  trpredmintr  9314  tcss  9338  tcel  9339  r1val1  9367  rankuni2b  9434  tcrank  9465  cardonle  9538  harval2  9578  ackbij2  9822  cfub  9828  cflecard  9832  cfflb  9838  isf32lem8  9939  itunitc1  9999  ttukeylem7  10094  fpwwe2lem8  10217  wuncss  10324  wuncval2  10326  grur1a  10398  trclfvub  14535  cotrtrclfv  14540  relexpfld  14577  rtrclreclem4  14589  limsupgre  15007  isercolllem3  15195  4sqlem19  16479  vdwlem1  16497  vdwlem12  16508  ramub1lem1  16542  setsstruct2  16703  ressress  16746  imasaddfnlem  16987  imasaddflem  16989  imasvscafn  16996  imasvscaf  16998  imasless  16999  isohom  17235  ressffth  17399  acsfiindd  18013  acsmap2d  18015  dirref  18061  mndind  18208  f1omvdco2  18794  pmtrfrn  18804  symgsssg  18813  symggen  18816  psgnunilem1  18839  sylow2alem2  18961  lsmssv  18986  smndlsmidm  18999  lsmidmOLD  19007  gsumzres  19248  dprdlub  19367  dprdf1  19374  dprdsn  19377  dprdcntz2  19379  dprd2dlem1  19382  dprd2da  19383  dmdprdsplit2lem  19386  ablfac1eu  19414  drnglpir  20245  znleval  20473  evpmss  20502  frlmsplit2  20689  f1lindf  20738  issubassa2  20806  mplsubglem  20915  evlslem4  20988  evlseu  20997  mhpaddcl  21045  mhpinvcl  21046  lpsscls  21992  tgrest  22010  resttopon  22012  rest0  22020  restfpw  22030  ordtrest  22053  ordtrest2  22055  lmcnp  22155  tgcmp  22252  uncmp  22254  hauscmplem  22257  1stcfb  22296  2ndcdisj  22307  dissnref  22379  kgencmp  22396  xkouni  22450  prdstopn  22479  txtube  22491  txcmplem2  22493  xkoptsub  22505  xkopt  22506  xkococnlem  22510  qtoprest  22568  imastopn  22571  kqdisj  22583  reghmph  22644  nrmhmph  22645  fbssfi  22688  trfilss  22740  trfg  22742  elfm3  22801  alexsubALTlem3  22900  alexsubALT  22902  cnextf  22917  cnextcn  22918  clsnsg  22961  tgpconncompeqg  22963  qustgphaus  22974  trust  23081  ustuqtop3  23095  neipcfilu  23147  metequiv2  23362  prdsxmslem2  23381  metustfbas  23409  icccmplem1  23673  metdstri  23702  pi1addf  23898  pi1addval  23899  caubl  24159  caublcls  24160  relcmpcmet  24169  minveclem4  24283  hlhil  24294  ovolficcss  24320  uniioombllem3a  24435  uniioombllem3  24436  dyadss  24445  opnmbllem  24452  i1fima2  24530  limcfval  24723  dvfval  24748  dvnres  24782  dvivth  24861  lhop  24867  taylf  25207  xrlimcnp  25805  jensen  25825  ppisval  25940  chtlepsi  26041  chpub  26055  iscgrglt  26559  chssoc  29531  mdsl0  30345  mdexchi  30370  atcvat3i  30431  dmdbr5ati  30457  funimass4f  30645  xrofsup  30764  swrdrn2  30900  gsumpart  30988  pmtrcnel  31031  tocycfvres1  31050  tocycfvres2  31051  cycpmco2lem6  31071  cycpmconjvlem  31081  cycpmconjslem2  31095  nsgmgc  31265  idlsrgmulrss1  31324  idlsrgmulrss2  31325  fedgmullem1  31378  fedgmullem2  31379  ist0cld  31451  locfinreflem  31458  cmpcref  31468  zarcls0  31486  zarclsiin  31489  zarcmplem  31499  cnvordtrestixx  31531  ordtrestNEW  31539  ordtrest2NEW  31541  pnfneige0  31569  sigagenss  31783  imambfm  31895  dya2iocress  31907  dya2icoseg  31910  dya2iocucvr  31917  ballotlemro  32155  ftc2re  32244  bnj1097  32628  bnj1452  32699  cvmlift3lem6  32953  msubrn  33158  mclsssv  33193  mclsind  33199  noextend  33555  nosupbday  33594  noinfbday  33609  scutun12  33690  scutbdaybnd  33695  scutbdaybnd2  33696  scutbdaylt  33698  cofcut1  33776  cofcutr  33778  liness  34133  neibastop2lem  34235  opnmbllem0  35499  mblfinlem2  35501  isbndx  35626  isbnd2  35627  ssbnd  35632  heiborlem3  35657  igenmin  35908  lsatlss  36696  lsmsat  36708  lsatfixedN  36709  lssats  36712  lpssat  36713  lssatle  36715  lssat  36716  lsatcvat3  36752  paddssat  37514  paddasslem17  37536  pmodlem2  37547  hlmod1i  37556  pl42lem4N  37682  diassdvaN  38760  dia2dimlem10  38773  cdlemn4a  38899  cdlemn5pre  38900  dihord5apre  38962  lclkrlem2e  39211  lclkrlem2p  39222  lclkrlem2v  39228  lclkrslem2  39238  lclkrs  39239  lcfrlem25  39267  lcfrlem35  39277  mapdval2N  39330  mapdpglem8  39379  mapdpglem13  39384  baerlem3lem2  39410  mapdindp2  39421  hdmap11lem2  39542  elrfi  40160  isnacs3  40176  mzpf  40202  mzpindd  40212  diophrw  40225  eldiophss  40240  rmxyelqirr  40376  pw2f1ocnv  40503  aomclem6  40528  hbt  40599  rgspnmin  40640  cnvssb  40811  trclubgNEW  40843  dfrcl2  40900  fvmptiunrelexplb0da  40911  relexp0a  40942  cotrcltrcl  40951  trclimalb2  40952  cotrclrcl  40968  isotone2  41277  k0004ss1  41379  fnresdmss  42318  mptelpm  42326  ssnnf1octb  42347  uzfissfz  42479  iuneqfzuzlem  42487  xlimliminflimsup  43021  icccncfext  43046  dvnprodlem1  43105  dvnprodlem2  43106  dvnprodlem3  43107  fourierdlem41  43307  fourierdlem70  43335  fourierdlem71  43336  fourierdlem80  43345  fourierdlem113  43378  ioorrnopnlem  43463  ioorrnopnxrlem  43465  salgenss  43493  dfsalgen2  43498  subsaliuncllem  43514  iundjiun  43616  meadjiunlem  43621  meaiunlelem  43624  meaiuninclem  43636  meaiininclem  43642  omeunle  43672  carageniuncllem2  43678  caratheodorylem1  43682  caratheodorylem2  43683  hoissre  43700  ovnsubaddlem1  43726  hoidmvlelem3  43753  ovnhoilem1  43757  ovnhoilem2  43758  ovnhoi  43759  ovncvr2  43767  voncmpl  43777  hspmbllem2  43783  hspmbl  43785  opnvonmbllem1  43788  vonmblss  43796  ovnsubadd2lem  43801  vonioolem2  43837  preimageiingt  43872  preimaleiinlt  43873  issmfd  43886  issmfdf  43888  sssmf  43889  cnfsmf  43891  issmfled  43908  issmfgtd  43911  smfadd  43915  smfrec  43938  smfmul  43944  smfmulc1  43945  smfpimbor1lem2  43948  smfsuplem1  43959  smflimsuplem1  43968  smflimsuplem7  43974  sprssspr  44549  linc1  45382