Theorem eqsstrd 3949

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  eqsstrrd  3950  eqsstrdi  3959  3sstr4d  3970  fpr2g  7155  tfisi  7799  suppssof1  8139  suppss2  8140  onfununi  8271  oawordeulem  8479  oeeui  8528  nnawordex  8563  oaabslem  8573  oaabs2  8575  omabslem  8576  omabs  8577  cofonr  8600  pw2f1olem  9009  fodomr  9056  fodomfir  9228  fival  9315  dffi3  9334  ordtypelem7  9429  ordtypelem8  9430  wemapso2lem  9457  cantnflt2  9585  cantnflem1  9601  tcss  9654  tcel  9655  r1val1  9701  rankuni2b  9768  tcrank  9799  cardonle  9872  harval2  9912  ackbij2  10155  cfub  10162  cflecard  10166  cfflb  10172  isf32lem8  10273  itunitc1  10333  ttukeylem7  10428  fpwwe2lem8  10552  wuncss  10659  wuncval2  10661  grur1a  10733  trclfvub  14960  cotrtrclfv  14965  relexpfld  15002  rtrclreclem4  15014  limsupgre  15434  isercolllem3  15620  4sqlem19  16925  vdwlem1  16943  vdwlem12  16954  ramub1lem1  16988  setsstruct2  17135  ressress  17208  imasaddfnlem  17483  imasaddflem  17485  imasvscafn  17492  imasvscaf  17494  imasless  17495  isohom  17734  ressffth  17898  acsfiindd  18510  acsmap2d  18512  dirref  18558  mndind  18787  f1omvdco2  19414  pmtrfrn  19424  symgsssg  19433  symggen  19436  psgnunilem1  19459  sylow2alem2  19584  lsmssv  19609  smndlsmidm  19622  gsumzres  19875  dprdlub  19994  dprdf1  20001  dprdsn  20004  dprdcntz2  20006  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  ablfac1eu  20041  rgspnmin  20587  drnglpir  21325  znleval  21529  evpmss  21561  frlmsplit2  21748  f1lindf  21797  issubassa2  21867  mplsubglem  21973  evlslem4  22052  evlseu  22059  mhpaddcl  22139  mhpinvcl  22140  psdmul  22154  lpsscls  23124  tgrest  23142  resttopon  23144  rest0  23152  restfpw  23162  ordtrest  23185  ordtrest2  23187  lmcnp  23287  tgcmp  23384  uncmp  23386  hauscmplem  23389  1stcfb  23428  2ndcdisj  23439  dissnref  23511  kgencmp  23528  xkouni  23582  prdstopn  23611  txtube  23623  txcmplem2  23625  xkoptsub  23637  xkopt  23638  xkococnlem  23642  qtoprest  23700  imastopn  23703  kqdisj  23715  reghmph  23776  nrmhmph  23777  fbssfi  23820  trfilss  23872  trfg  23874  elfm3  23933  alexsubALTlem3  24032  alexsubALT  24034  cnextf  24049  cnextcn  24050  clsnsg  24093  tgpconncompeqg  24095  qustgphaus  24106  trust  24212  ustuqtop3  24226  neipcfilu  24278  metequiv2  24493  prdsxmslem2  24512  metustfbas  24540  icccmplem1  24806  metdstri  24835  pi1addf  25032  pi1addval  25033  caubl  25293  caublcls  25294  relcmpcmet  25303  minveclem4  25417  hlhil  25428  ovolficcss  25454  uniioombllem3a  25569  uniioombllem3  25570  dyadss  25579  opnmbllem  25586  i1fima2  25664  limcfval  25857  dvfval  25882  dvnres  25916  dvivth  25995  lhop  26001  taylf  26344  xrlimcnp  26950  jensen  26970  ppisval  27085  chtlepsi  27187  chpub  27201  noextend  27648  nosupbday  27687  noinfbday  27702  cutsun12  27800  cutbdaybnd  27805  cutbdaybnd2  27806  cutbdaylt  27808  sltsbday  27927  cofcut1  27930  cofcutr  27934  addbday  28028  negbdaylem  28066  precsexlem8  28224  bdayons  28286  onsbnd2  28292  noseqind  28302  n0bday  28362  bdaypw2n0bndlem  28473  iscgrglt  28600  cyclnumvtx  29886  chssoc  31585  mdsl0  32399  mdexchi  32424  atcvat3i  32485  dmdbr5ati  32511  funimass4f  32729  xrofsup  32859  swrdrn2  33033  gsumpart  33144  pmtrcnel  33170  tocycfvres1  33191  tocycfvres2  33192  cycpmco2lem6  33212  cycpmconjvlem  33222  cycpmconjslem2  33236  elrgspnsubrunlem2  33329  fldgenssv  33399  fldgenssp  33402  nsgmgc  33495  idlsrgmulrss1  33594  idlsrgmulrss2  33595  esplyfval1  33757  esplyfvaln  33758  esplyind  33759  fedgmullem1  33813  fedgmullem2  33814  constrsscn  33924  constrmon  33928  ist0cld  34017  locfinreflem  34024  cmpcref  34034  zarcls0  34052  zarclsiin  34055  zarcmplem  34065  cnvordtrestixx  34097  ordtrestNEW  34105  ordtrest2NEW  34107  pnfneige0  34135  sigagenss  34333  imambfm  34446  dya2iocress  34458  dya2icoseg  34461  dya2iocucvr  34468  ballotlemro  34707  ftc2re  34782  bnj1097  35163  bnj1452  35234  cvmlift3lem6  35552  msubrn  35757  mclsssv  35792  mclsind  35798  liness  36373  neibastop2lem  36588  ttcmin  36724  dfttc3gw  36751  opnmbllem0  38023  mblfinlem2  38025  isbndx  38149  isbnd2  38150  ssbnd  38155  heiborlem3  38180  igenmin  38431  lsatlss  39488  lsmsat  39500  lsatfixedN  39501  lssats  39504  lpssat  39505  lssatle  39507  lssat  39508  lsatcvat3  39544  paddssat  40306  paddasslem17  40328  pmodlem2  40339  hlmod1i  40348  pl42lem4N  40474  diassdvaN  41552  dia2dimlem10  41565  cdlemn4a  41691  cdlemn5pre  41692  dihord5apre  41754  lclkrlem2e  42003  lclkrlem2p  42014  lclkrlem2v  42020  lclkrslem2  42030  lclkrs  42031  lcfrlem25  42059  lcfrlem35  42069  mapdval2N  42122  mapdpglem8  42171  mapdpglem13  42176  baerlem3lem2  42202  mapdindp2  42213  hdmap11lem2  42334  primrootspoweq0  42591  aks6d1c6lem2  42656  evlsmhpvvval  43045  prjspnssbas  43071  elrfi  43143  isnacs3  43159  mzpf  43185  mzpindd  43195  diophrw  43208  eldiophss  43223  pw2f1ocnv  43482  aomclem6  43504  hbt  43575  oasubex  43731  oaabsb  43739  nnoeomeqom  43757  omcl2  43778  naddgeoa  43839  naddwordnexlem4  43846  oaltom  43849  omltoe  43851  minregex  43978  cnvssb  44030  trclubgNEW  44062  dfrcl2  44118  fvmptiunrelexplb0da  44129  relexp0a  44160  cotrcltrcl  44169  trclimalb2  44170  cotrclrcl  44186  isotone2  44493  k0004ss1  44595  fnresdmss  45615  mptelpm  45623  ssnnf1octb  45641  uzfissfz  45771  iuneqfzuzlem  45779  xlimliminflimsup  46305  icccncfext  46330  dvnprodlem2  46390  dvnprodlem3  46391  fourierdlem41  46591  fourierdlem70  46619  fourierdlem71  46620  fourierdlem80  46629  fourierdlem113  46662  ioorrnopnlem  46747  ioorrnopnxrlem  46749  salgenss  46779  dfsalgen2  46784  subsaliuncllem  46800  iundjiun  46903  meadjiunlem  46908  meaiunlelem  46911  meaiuninclem  46923  meaiininclem  46929  omeunle  46959  carageniuncllem2  46965  caratheodorylem1  46969  caratheodorylem2  46970  hoissre  46987  ovnsubaddlem1  47013  hoidmvlelem3  47040  ovnhoilem1  47044  ovnhoilem2  47045  ovnhoi  47046  ovncvr2  47054  voncmpl  47064  hspmbllem2  47070  hspmbl  47072  opnvonmbllem1  47075  vonmblss  47083  ovnsubadd2lem  47088  vonioolem2  47124  preimaleiinlt  47164  issmfd  47178  issmfdf  47180  sssmf  47181  cnfsmf  47183  issmfled  47200  issmfgtd  47204  smfadd  47208  smfrec  47232  smfmul  47238  smfmulc1  47239  smfpimbor1lem2  47242  smfsuplem1  47254  smflimsuplem1  47263  smflimsuplem7  47269  sprssspr  47956  isubgredgss  48356  isubgrsubgr  48360  uhgrimisgrgriclem  48421  stgrnbgr0  48455  uspgrlimlem3  48481  linc1  48916  iinfssc  49547  discsubc  49554  idfullsubc  49651