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 259	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  eqsstrrd  3969  eqsstrdi  3978  3sstr4d  3989  fpr2g  7190  tfisi  7834  suppssof1  8173  suppss2  8174  onfununi  8306  oawordeulem  8517  oeeui  8566  nnawordex  8601  oaabslem  8611  oaabs2  8613  omabslem  8614  omabs  8615  cofonr  8638  pw2f1olem  9047  fodomr  9094  fodomfir  9266  fival  9352  dffi3  9371  ordtypelem7  9466  ordtypelem8  9467  wemapso2lem  9494  cantnflt2  9622  cantnflem1  9638  tcss  9691  tcel  9692  r1val1  9738  rankuni2b  9805  tcrank  9836  cardonle  9909  harval2  9949  ackbij2  10192  cfub  10199  cflecard  10203  cfflb  10210  isf32lem8  10311  itunitc1  10371  ttukeylem7  10466  fpwwe2lem8  10590  wuncss  10697  wuncval2  10699  grur1a  10771  trclfvub  15014  cotrtrclfv  15019  relexpfld  15056  rtrclreclem4  15068  limsupgre  15499  isercolllem3  15685  4sqlem19  16990  vdwlem1  17008  vdwlem12  17019  ramub1lem1  17053  setsstruct2  17201  ressress  17274  imasaddfnlem  17549  imasaddflem  17551  imasvscafn  17558  imasvscaf  17560  imasless  17561  isohom  17800  ressffth  17964  acsfiindd  18576  acsmap2d  18578  dirref  18624  mndind  18853  f1omvdco2  19479  pmtrfrn  19489  symgsssg  19498  symggen  19501  psgnunilem1  19524  sylow2alem2  19649  lsmssv  19674  smndlsmidm  19687  gsumzres  19940  dprdlub  20059  dprdf1  20066  dprdsn  20069  dprdcntz2  20071  dprd2dlem1  20074  dprd2da  20075  dmdprdsplit2lem  20078  ablfac1eu  20106  rgspnmin  20652  drnglpir  21390  znleval  21594  evpmss  21626  frlmsplit2  21813  f1lindf  21862  issubassa2  21932  mplsubglem  22038  evlslem4  22117  evlseu  22124  mhpaddcl  22204  mhpinvcl  22205  psdmul  22219  lpsscls  23189  tgrest  23207  resttopon  23209  rest0  23217  restfpw  23227  ordtrest  23250  ordtrest2  23252  lmcnp  23352  tgcmp  23449  uncmp  23451  hauscmplem  23454  1stcfb  23493  2ndcdisj  23504  dissnref  23576  kgencmp  23593  xkouni  23647  prdstopn  23676  txtube  23688  txcmplem2  23690  xkoptsub  23702  xkopt  23703  xkococnlem  23707  qtoprest  23765  imastopn  23768  kqdisj  23780  reghmph  23841  nrmhmph  23842  fbssfi  23885  trfilss  23937  trfg  23939  elfm3  23998  alexsubALTlem3  24097  alexsubALT  24099  cnextf  24114  cnextcn  24115  clsnsg  24158  tgpconncompeqg  24160  qustgphaus  24171  trust  24277  ustuqtop3  24291  neipcfilu  24343  metequiv2  24558  prdsxmslem2  24577  metustfbas  24605  icccmplem1  24871  metdstri  24900  pi1addf  25097  pi1addval  25098  caubl  25358  caublcls  25359  relcmpcmet  25368  minveclem4  25482  hlhil  25493  ovolficcss  25519  uniioombllem3a  25634  uniioombllem3  25635  dyadss  25644  opnmbllem  25651  i1fima2  25729  limcfval  25922  dvfval  25947  dvnres  25981  dvivth  26060  lhop  26066  taylf  26412  xrlimcnp  27021  jensen  27041  ppisval  27156  chtlepsi  27258  chpub  27272  noextend  27718  nosupbday  27757  noinfbday  27772  cutsun12  27871  cutbdaybnd  27876  cutbdaybnd2  27877  cutbdaylt  27879  sltsbday  27998  cofcut1  28001  cofcutr  28005  addbday  28099  negbdaylem  28137  precsexlem8  28295  bdayons  28357  onsbnd2  28363  noseqind  28373  n0bday  28433  bdaypw2n0bndlem  28544  iscgrglt  28671  cyclnumvtx  29957  chssoc  31656  mdsl0  32470  mdexchi  32495  atcvat3i  32556  dmdbr5ati  32582  funimass4f  32800  xrofsup  32930  swrdrn2  33093  gsumpart  33204  pmtrcnel  33230  tocycfvres1  33251  tocycfvres2  33252  cycpmco2lem6  33272  cycpmconjvlem  33282  cycpmconjslem2  33296  elrgspnsubrunlem2  33390  fldgenssv  33463  fldgenssp  33466  nsgmgc  33559  idlsrgmulrss1  33668  idlsrgmulrss2  33669  esplyfval1  33831  esplyfvaln  33832  esplyind  33833  fedgmullem1  33887  fedgmullem2  33888  constrsscn  33998  constrmon  34002  ist0cld  34091  locfinreflem  34098  cmpcref  34108  zarcls0  34126  zarclsiin  34129  zarcmplem  34139  cnvordtrestixx  34171  ordtrestNEW  34179  ordtrest2NEW  34181  pnfneige0  34209  sigagenss  34407  imambfm  34520  dya2iocress  34532  dya2icoseg  34535  dya2iocucvr  34542  ballotlemro  34781  ftc2re  34853  bnj1097  35237  bnj1452  35308  cvmlift3lem6  35635  msubrn  35840  mclsssv  35875  mclsind  35881  liness  36456  neibastop2lem  36681  ttcmin  36817  dfttc3gw  36844  opnmbllem0  38116  mblfinlem2  38118  isbndx  38242  isbnd2  38243  ssbnd  38248  heiborlem3  38273  igenmin  38524  lsatlss  39581  lsmsat  39593  lsatfixedN  39594  lssats  39597  lpssat  39598  lssatle  39600  lssat  39601  lsatcvat3  39637  paddssat  40399  paddasslem17  40421  pmodlem2  40432  hlmod1i  40441  pl42lem4N  40567  diassdvaN  41645  dia2dimlem10  41658  cdlemn4a  41784  cdlemn5pre  41785  dihord5apre  41847  lclkrlem2e  42096  lclkrlem2p  42107  lclkrlem2v  42113  lclkrslem2  42123  lclkrs  42124  lcfrlem25  42152  lcfrlem35  42162  mapdval2N  42215  mapdpglem8  42264  mapdpglem13  42269  baerlem3lem2  42295  mapdindp2  42306  hdmap11lem2  42427  primrootspoweq0  42684  aks6d1c6lem2  42749  evlsmhpvvval  43138  prjspnssbas  43164  elrfi  43236  isnacs3  43252  mzpf  43278  mzpindd  43288  diophrw  43301  eldiophss  43316  pw2f1ocnv  43575  aomclem6  43597  hbt  43668  oasubex  43824  oaabsb  43832  nnoeomeqom  43850  omcl2  43871  naddgeoa  43932  naddwordnexlem4  43939  oaltom  43942  omltoe  43944  minregex  44071  cnvssb  44123  trclubgNEW  44155  dfrcl2  44211  fvmptiunrelexplb0da  44222  relexp0a  44253  cotrcltrcl  44262  trclimalb2  44263  cotrclrcl  44279  isotone2  44586  k0004ss1  44688  fnresdmss  45707  mptelpm  45715  ssnnf1octb  45733  uzfissfz  45863  iuneqfzuzlem  45871  xlimliminflimsup  46397  icccncfext  46422  dvnprodlem2  46482  dvnprodlem3  46483  fourierdlem41  46683  fourierdlem70  46711  fourierdlem71  46712  fourierdlem80  46721  ioorrnopnlem  46839  ioorrnopnxrlem  46841  salgenss  46871  dfsalgen2  46876  subsaliuncllem  46892  iundjiun  46995  meadjiunlem  47000  meaiunlelem  47003  meaiuninclem  47015  meaiininclem  47021  omeunle  47051  carageniuncllem2  47057  caratheodorylem1  47061  caratheodorylem2  47062  hoissre  47079  ovnsubaddlem1  47105  hoidmvlelem3  47132  ovnhoilem1  47136  ovnhoilem2  47137  ovnhoi  47138  ovncvr2  47146  voncmpl  47156  hspmbllem2  47162  hspmbl  47164  opnvonmbllem1  47167  vonmblss  47175  ovnsubadd2lem  47180  vonioolem2  47216  preimaleiinlt  47256  issmfd  47270  issmfdf  47272  cnfsmf  47275  issmfled  47292  issmfgtd  47296  smfadd  47300  smfrec  47324  smfmul  47330  smfmulc1  47331  smfpimbor1lem2  47334  smfsuplem1  47346  smflimsuplem1  47355  smflimsuplem7  47361  sprssspr  48048  isubgredgss  48448  isubgrsubgr  48452  uhgrimisgrgriclem  48513  stgrnbgr0  48547  uspgrlimlem3  48573  linc1  49008  iinfssc  49639  discsubc  49646  idfullsubc  49743