Theorem eqsstrd 3972

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  eqsstrrd  3973  eqsstrdi  3982  3sstr4d  3993  fpr2g  7213  tfisi  7857  suppssof1  8197  suppss2  8198  onfununi  8330  oawordeulem  8541  oeeui  8590  nnawordex  8625  oaabslem  8635  oaabs2  8637  omabslem  8638  omabs  8639  cofonr  8662  pw2f1olem  9072  fodomr  9119  fodomfir  9290  fival  9375  dffi3  9394  ordtypelem7  9489  ordtypelem8  9490  wemapso2lem  9517  cantnflt2  9645  cantnflem1  9661  tcss  9714  tcel  9715  r1val1  9761  rankuni2b  9828  tcrank  9859  cardonle  9955  harval2  9995  ackbij2  10237  cfub  10243  cflecard  10247  cfflb  10254  isf32lem8  10355  itunitc1  10415  ttukeylem7  10510  fpwwe2lem8  10634  wuncss  10741  wuncval2  10743  grur1a  10815  trclfvub  15064  cotrtrclfv  15069  relexpfld  15106  rtrclreclem4  15118  limsupgre  15552  isercolllem3  15738  4sqlem19  17041  vdwlem1  17059  vdwlem12  17070  ramub1lem1  17104  setsstruct2  17252  ressress  17325  imasaddfnlem  17600  imasaddflem  17602  imasvscafn  17609  imasvscaf  17611  imasless  17612  isohom  17851  ressffth  18015  acsfiindd  18627  acsmap2d  18629  dirref  18675  mndind  18911  f1omvdco2  19542  pmtrfrn  19552  symgsssg  19561  symggen  19564  psgnunilem1  19587  sylow2alem2  19712  lsmssv  19737  smndlsmidm  19750  gsumzres  20003  dprdlub  20122  dprdf1  20129  dprdsn  20132  dprdcntz2  20134  dprd2dlem1  20137  dprd2da  20138  dmdprdsplit2lem  20141  ablfac1eu  20169  rgspnmin  20744  drnglpir  21530  znleval  21734  evpmss  21766  frlmsplit2  21953  f1lindf  22002  issubassa2  22072  mplsubglem  22178  evlslem4  22257  evlseu  22264  mhpaddcl  22344  mhpinvcl  22345  psdmul  22359  lpsscls  23328  tgrest  23346  resttopon  23348  rest0  23356  restfpw  23366  ordtrest  23389  ordtrest2  23391  lmcnp  23491  tgcmp  23588  uncmp  23590  hauscmplem  23593  1stcfb  23632  2ndcdisj  23644  dissnref  23716  kgencmp  23733  xkouni  23787  prdstopn  23816  txtube  23828  txcmplem2  23830  xkoptsub  23842  xkopt  23843  xkococnlem  23847  qtoprest  23905  imastopn  23908  kqdisj  23920  reghmph  23981  nrmhmph  23982  fbssfi  24025  trfilss  24077  trfg  24079  elfm3  24138  alexsubALTlem3  24237  alexsubALT  24239  cnextf  24254  cnextcn  24255  clsnsg  24298  tgpconncompeqg  24300  qustgphaus  24311  trust  24417  ustuqtop3  24431  neipcfilu  24483  metequiv2  24698  prdsxmslem2  24717  metustfbas  24745  icccmplem1  25011  metdstri  25040  pi1addf  25237  pi1addval  25238  caubl  25498  caublcls  25499  relcmpcmet  25508  minveclem4  25622  hlhil  25633  ovolficcss  25659  uniioombllem3a  25774  uniioombllem3  25775  dyadss  25784  opnmbllem  25791  i1fima2  25869  limcfval  26062  dvfval  26087  dvnres  26121  dvivth  26200  lhop  26206  taylf  26555  xrlimcnp  27164  jensen  27184  ppisval  27299  chtlepsi  27401  chpub  27415  noextend  27861  nosupbday  27900  noinfbday  27915  cutsun12  28014  cutbdaybnd  28019  cutbdaybnd2  28020  cutbdaylt  28022  sltsbday  28141  cofcut1  28144  cofcutr  28148  addbday  28242  negbdaylem  28280  precsexlem8  28438  bdayons  28500  onsbnd2  28506  noseqind  28516  n0bday  28576  bdaypw2n0bndlem  28687  iscgrglt  28814  cyclnumvtx  30191  chssoc  31895  mdsl0  32709  mdexchi  32734  atcvat3i  32795  dmdbr5ati  32821  funimass4f  33029  xrofsup  33158  swrdrn2  33316  gsumpart  33423  pmtrcnel  33449  tocycfvres1  33470  tocycfvres2  33471  cycpmco2lem6  33491  cycpmconjvlem  33501  cycpmconjslem2  33515  elrgspnsubrunlem2  33608  fldgenssv  33676  fldgenssp  33679  nsgmgc  33761  idlsrgmulrss1  33841  idlsrgmulrss2  33842  esplyfval1  34003  esplyfvaln  34004  esplyind  34005  fedgmullem1  34059  fedgmullem2  34060  constrsscn  34170  constrmon  34174  ist0cld  34263  locfinreflem  34270  cmpcref  34280  zarcls0  34298  zarclsiin  34301  zarcmplem  34311  cnvordtrestixx  34343  ordtrestNEW  34351  ordtrest2NEW  34353  pnfneige0  34381  sigagenss  34580  imambfm  34693  dya2iocress  34705  dya2icoseg  34708  dya2iocucvr  34715  ballotlemro  34954  ftc2re  35026  bnj1097  35410  bnj1452  35481  rankscottu  35556  cvmlift3lem6  35829  msubrn  36034  mclsssv  36069  mclsind  36075  liness  36650  neibastop2lem  36904  ttcmin  37040  dfttc3gw  37067  opnmbllem0  38340  mblfinlem2  38342  isbndx  38466  isbnd2  38467  ssbnd  38472  heiborlem3  38497  igenmin  38748  lsatlss  39803  lsmsat  39815  lsatfixedN  39816  lssats  39819  lpssat  39820  lssatle  39822  lssat  39823  lsatcvat3  39859  paddssat  40621  paddasslem17  40643  pmodlem2  40654  hlmod1i  40663  pl42lem4N  40789  diassdvaN  41867  dia2dimlem10  41880  cdlemn4a  42006  cdlemn5pre  42007  dihord5apre  42069  lclkrlem2e  42318  lclkrlem2p  42329  lclkrlem2v  42335  lclkrslem2  42345  lclkrs  42346  lcfrlem25  42374  lcfrlem35  42384  mapdval2N  42437  mapdpglem8  42486  mapdpglem13  42491  baerlem3lem2  42517  mapdindp2  42528  hdmap11lem2  42649  primrootspoweq0  42906  aks6d1c6lem2  42971  evlsmhpvvval  43360  prjspnssbas  43386  elrfi  43458  isnacs3  43474  mzpf  43500  mzpindd  43510  diophrw  43523  eldiophss  43538  pw2f1ocnv  43797  aomclem6  43819  hbt  43890  oasubex  44046  oaabsb  44054  nnoeomeqom  44072  omcl2  44093  naddgeoa  44154  naddwordnexlem4  44161  oaltom  44164  omltoe  44166  minregex  44293  cnvssb  44345  trclubgNEW  44377  dfrcl2  44433  fvmptiunrelexplb0da  44444  relexp0a  44475  cotrcltrcl  44484  trclimalb2  44485  cotrclrcl  44501  isotone2  44808  k0004ss1  44910  fnresdmss  45919  mptelpm  45927  ssnnf1octb  45945  uzfissfz  46075  iuneqfzuzlem  46083  xlimliminflimsup  46609  icccncfext  46634  dvnprodlem2  46694  dvnprodlem3  46695  fourierdlem41  46895  fourierdlem70  46923  fourierdlem71  46924  fourierdlem80  46933  ioorrnopnlem  47051  ioorrnopnxrlem  47053  salgenss  47083  dfsalgen2  47088  subsaliuncllem  47104  iundjiun  47207  meadjiunlem  47212  meaiunlelem  47215  meaiuninclem  47227  meaiininclem  47233  omeunle  47263  carageniuncllem2  47269  caratheodorylem1  47273  caratheodorylem2  47274  hoissre  47291  ovnsubaddlem1  47317  hoidmvlelem3  47344  ovnhoilem1  47348  ovnhoilem2  47349  ovnhoi  47350  ovncvr2  47358  voncmpl  47368  hspmbllem2  47374  hspmbl  47376  opnvonmbllem1  47379  vonmblss  47387  ovnsubadd2lem  47392  vonioolem2  47428  preimaleiinlt  47468  issmfd  47482  issmfdf  47484  cnfsmf  47487  issmfled  47504  issmfgtd  47508  smfadd  47512  smfrec  47536  smfmul  47542  smfmulc1  47543  smfpimbor1lem2  47546  smfsuplem1  47558  smflimsuplem1  47567  smflimsuplem7  47573  sprssspr  48263  isubgredgss  48663  isubgrsubgr  48667  uhgrimisgrgriclem  48728  stgrnbgr0  48762  uspgrlimlem3  48788  linc1  49238  iinfssc  49868  discsubc  49875  idfullsubc  49972