Theorem eqsstrd 4020

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  eqsstrrd  4021  eqsstrdi  4036  fpr2g  7215  tfisi  7850  suppssof1  8186  suppss2  8187  onfununi  8343  oawordeulem  8556  oeeui  8604  nnawordex  8639  oaabslem  8648  oaabs2  8650  omabslem  8651  omabs  8652  cofonr  8675  pw2f1olem  9078  fodomr  9130  fival  9409  dffi3  9428  ordtypelem7  9521  ordtypelem8  9522  wemapso2lem  9549  cantnflt2  9670  cantnflem1  9686  tcss  9741  tcel  9742  r1val1  9783  rankuni2b  9850  tcrank  9881  cardonle  9954  harval2  9994  ackbij2  10240  cfub  10246  cflecard  10250  cfflb  10256  isf32lem8  10357  itunitc1  10417  ttukeylem7  10512  fpwwe2lem8  10635  wuncss  10742  wuncval2  10744  grur1a  10816  trclfvub  14958  cotrtrclfv  14963  relexpfld  15000  rtrclreclem4  15012  limsupgre  15429  isercolllem3  15617  4sqlem19  16900  vdwlem1  16918  vdwlem12  16929  ramub1lem1  16963  setsstruct2  17111  ressress  17197  imasaddfnlem  17478  imasaddflem  17480  imasvscafn  17487  imasvscaf  17489  imasless  17490  isohom  17727  ressffth  17893  acsfiindd  18510  acsmap2d  18512  dirref  18558  mndind  18745  f1omvdco2  19357  pmtrfrn  19367  symgsssg  19376  symggen  19379  psgnunilem1  19402  sylow2alem2  19527  lsmssv  19552  smndlsmidm  19565  gsumzres  19818  dprdlub  19937  dprdf1  19944  dprdsn  19947  dprdcntz2  19949  dprd2dlem1  19952  dprd2da  19953  dmdprdsplit2lem  19956  ablfac1eu  19984  drnglpir  21091  znleval  21329  evpmss  21358  frlmsplit2  21547  f1lindf  21596  issubassa2  21665  mplsubglem  21777  evlslem4  21856  evlseu  21865  mhpaddcl  21913  mhpinvcl  21914  lpsscls  22865  tgrest  22883  resttopon  22885  rest0  22893  restfpw  22903  ordtrest  22926  ordtrest2  22928  lmcnp  23028  tgcmp  23125  uncmp  23127  hauscmplem  23130  1stcfb  23169  2ndcdisj  23180  dissnref  23252  kgencmp  23269  xkouni  23323  prdstopn  23352  txtube  23364  txcmplem2  23366  xkoptsub  23378  xkopt  23379  xkococnlem  23383  qtoprest  23441  imastopn  23444  kqdisj  23456  reghmph  23517  nrmhmph  23518  fbssfi  23561  trfilss  23613  trfg  23615  elfm3  23674  alexsubALTlem3  23773  alexsubALT  23775  cnextf  23790  cnextcn  23791  clsnsg  23834  tgpconncompeqg  23836  qustgphaus  23847  trust  23954  ustuqtop3  23968  neipcfilu  24021  metequiv2  24239  prdsxmslem2  24258  metustfbas  24286  icccmplem1  24558  metdstri  24587  pi1addf  24787  pi1addval  24788  caubl  25049  caublcls  25050  relcmpcmet  25059  minveclem4  25173  hlhil  25184  ovolficcss  25210  uniioombllem3a  25325  uniioombllem3  25326  dyadss  25335  opnmbllem  25342  i1fima2  25420  limcfval  25613  dvfval  25638  dvnres  25672  dvivth  25751  lhop  25757  taylf  26097  xrlimcnp  26697  jensen  26717  ppisval  26832  chtlepsi  26933  chpub  26947  noextend  27393  nosupbday  27432  noinfbday  27447  scutun12  27536  scutbdaybnd  27541  scutbdaybnd2  27542  scutbdaylt  27544  cofcut1  27633  cofcutr  27637  negsbdaylem  27757  precsexlem8  27887  iscgrglt  28020  chssoc  31004  mdsl0  31818  mdexchi  31843  atcvat3i  31904  dmdbr5ati  31930  funimass4f  32116  xrofsup  32235  swrdrn2  32373  gsumpart  32465  pmtrcnel  32508  tocycfvres1  32527  tocycfvres2  32528  cycpmco2lem6  32548  cycpmconjvlem  32558  cycpmconjslem2  32572  fldgenssv  32663  fldgenssp  32666  nsgmgc  32785  idlsrgmulrss1  32887  idlsrgmulrss2  32888  fedgmullem1  32990  fedgmullem2  32991  ist0cld  33099  locfinreflem  33106  cmpcref  33116  zarcls0  33134  zarclsiin  33137  zarcmplem  33147  cnvordtrestixx  33179  ordtrestNEW  33187  ordtrest2NEW  33189  pnfneige0  33217  sigagenss  33433  imambfm  33547  dya2iocress  33559  dya2icoseg  33562  dya2iocucvr  33569  ballotlemro  33807  ftc2re  33896  bnj1097  34278  bnj1452  34349  cvmlift3lem6  34601  msubrn  34806  mclsssv  34841  mclsind  34847  liness  35409  neibastop2lem  35548  opnmbllem0  36827  mblfinlem2  36829  isbndx  36953  isbnd2  36954  ssbnd  36959  heiborlem3  36984  igenmin  37235  lsatlss  38169  lsmsat  38181  lsatfixedN  38182  lssats  38185  lpssat  38186  lssatle  38188  lssat  38189  lsatcvat3  38225  paddssat  38988  paddasslem17  39010  pmodlem2  39021  hlmod1i  39030  pl42lem4N  39156  diassdvaN  40234  dia2dimlem10  40247  cdlemn4a  40373  cdlemn5pre  40374  dihord5apre  40436  lclkrlem2e  40685  lclkrlem2p  40696  lclkrlem2v  40702  lclkrslem2  40712  lclkrs  40713  lcfrlem25  40741  lcfrlem35  40751  mapdval2N  40804  mapdpglem8  40853  mapdpglem13  40858  baerlem3lem2  40884  mapdindp2  40895  hdmap11lem2  41016  evlsmhpvvval  41469  prjspnssbas  41665  elrfi  41734  isnacs3  41750  mzpf  41776  mzpindd  41786  diophrw  41799  eldiophss  41814  rmxyelqirrOLD  41951  pw2f1ocnv  42078  aomclem6  42103  hbt  42174  rgspnmin  42215  oasubex  42338  oaabsb  42346  nnoeomeqom  42364  omcl2  42385  naddgeoa  42447  naddwordnexlem4  42454  oaltom  42458  omltoe  42460  minregex  42587  cnvssb  42639  trclubgNEW  42671  dfrcl2  42727  fvmptiunrelexplb0da  42738  relexp0a  42769  cotrcltrcl  42778  trclimalb2  42779  cotrclrcl  42795  isotone2  43102  k0004ss1  43204  fnresdmss  44166  mptelpm  44174  ssnnf1octb  44192  uzfissfz  44335  iuneqfzuzlem  44343  xlimliminflimsup  44877  icccncfext  44902  dvnprodlem1  44961  dvnprodlem2  44962  dvnprodlem3  44963  fourierdlem41  45163  fourierdlem70  45191  fourierdlem71  45192  fourierdlem80  45201  fourierdlem113  45234  ioorrnopnlem  45319  ioorrnopnxrlem  45321  salgenss  45351  dfsalgen2  45356  subsaliuncllem  45372  iundjiun  45475  meadjiunlem  45480  meaiunlelem  45483  meaiuninclem  45495  meaiininclem  45501  omeunle  45531  carageniuncllem2  45537  caratheodorylem1  45541  caratheodorylem2  45542  hoissre  45559  ovnsubaddlem1  45585  hoidmvlelem3  45612  ovnhoilem1  45616  ovnhoilem2  45617  ovnhoi  45618  ovncvr2  45626  voncmpl  45636  hspmbllem2  45642  hspmbl  45644  opnvonmbllem1  45647  vonmblss  45655  ovnsubadd2lem  45660  vonioolem2  45696  preimageiingt  45735  preimaleiinlt  45736  issmfd  45750  issmfdf  45752  sssmf  45753  cnfsmf  45755  issmfled  45772  issmfgtd  45776  smfadd  45780  smfrec  45804  smfmul  45810  smfmulc1  45811  smfpimbor1lem2  45814  smfsuplem1  45826  smflimsuplem1  45835  smflimsuplem7  45841  sprssspr  46448  linc1  47194