Theorem eqsstrd 3965

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

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

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 2155  ax-ext 2732

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

This theorem is used by:  eqsstrrd  3966  eqsstrdi  3975  3sstr4d  3986  fpr2g  7210  tfisi  7855  suppssof1  8197  suppss2  8198  onfununi  8330  oawordeulem  8541  oeeui  8590  nnawordex  8625  oaabslem  8635  oaabs2  8637  omabslem  8638  omabs  8639  cofonr  8662  pw2f1olem  9079  fodomr  9126  fodomfir  9297  fival  9382  dffi3  9401  ordtypelem7  9496  ordtypelem8  9497  wemapso2lem  9524  cantnflt2  9652  cantnflem1  9668  tcss  9721  tcel  9722  r1val1  9768  rankuni2b  9835  tcrank  9866  cardonle  9962  harval2  10002  ackbij2  10244  cfub  10250  cflecard  10254  cfflb  10261  isf32lem8  10362  itunitc1  10422  ttukeylem7  10517  fpwwe2lem8  10647  wuncss  10754  wuncval2  10756  grur1a  10828  trclfvub  15080  cotrtrclfv  15085  relexpfld  15122  rtrclreclem4  15134  limsupgre  15568  isercolllem3  15754  4sqlem19  17055  vdwlem1  17073  vdwlem12  17084  ramub1lem1  17118  setsstruct2  17266  ressress  17339  imasaddfnlem  17614  imasaddflem  17616  imasvscafn  17623  imasvscaf  17625  imasless  17626  isohom  17865  ressffth  18029  acsfiindd  18641  acsmap2d  18643  dirref  18689  mndind  18937  f1omvdco2  19575  pmtrfrn  19585  symgsssg  19594  symggen  19597  psgnunilem1  19620  sylow2alem2  19745  lsmssv  19770  smndlsmidm  19783  gsumzres  20036  dprdlub  20155  dprdf1  20162  dprdsn  20165  dprdcntz2  20167  dprd2dlem1  20170  dprd2da  20171  dmdprdsplit2lem  20174  ablfac1eu  20202  rgspnmin  20777  drnglpir  21563  znleval  21767  evpmss  21799  frlmsplit2  21986  f1lindf  22035  issubassa2  22107  mplsubglem  22213  evlslem4  22292  evlseu  22299  mhpaddcl  22379  mhpinvcl  22380  psdmul  22394  lpsscls  23366  tgrest  23384  resttopon  23386  rest0  23394  restfpw  23404  ordtrest  23427  ordtrest2  23429  lmcnp  23529  tgcmp  23626  uncmp  23628  hauscmplem  23631  1stcfb  23670  2ndcdisj  23682  dissnref  23754  kgencmp  23771  xkouni  23825  prdstopn  23854  txtube  23866  txcmplem2  23868  xkoptsub  23880  xkopt  23881  xkococnlem  23885  qtoprest  23943  imastopn  23946  kqdisj  23958  reghmph  24019  nrmhmph  24020  fbssfi  24063  trfilss  24115  trfg  24117  elfm3  24176  alexsubALTlem3  24275  alexsubALT  24277  cnextf  24292  cnextcn  24293  clsnsg  24336  tgpconncompeqg  24338  qustgphaus  24349  trust  24455  ustuqtop3  24469  neipcfilu  24521  metequiv2  24736  prdsxmslem2  24755  metustfbas  24783  icccmplem1  25049  metdstri  25078  pi1addf  25275  pi1addval  25276  caubl  25536  caublcls  25537  relcmpcmet  25546  minveclem4  25660  hlhil  25671  ovolficcss  25697  uniioombllem3a  25812  uniioombllem3  25813  dyadss  25822  opnmbllem  25829  i1fima2  25907  limcfval  26099  dvfval  26124  dvnres  26158  dvivth  26237  lhop  26243  taylf  26597  xrlimcnp  27205  jensen  27225  ppisval  27340  chtlepsi  27442  chpub  27456  noextend  27902  nosupbday  27941  noinfbday  27956  cutsun12  28055  cutbdaybnd  28060  cutbdaybnd2  28061  cutbdaylt  28063  sltsbday  28182  cofcut1  28185  cofcutr  28189  addbday  28283  negbdaylem  28321  precsexlem8  28479  bdayons  28541  onsbnd2  28547  noseqind  28557  n0bday  28617  bdaypw2n0bndlem  28728  iscgrglt  28856  cyclnumvtx  30267  chssoc  31977  mdsl0  32791  mdexchi  32816  atcvat3i  32877  dmdbr5ati  32903  funimass4f  33110  xrofsup  33238  swrdrn2  33396  gsumpart  33503  pmtrcnel  33529  tocycfvres1  33550  tocycfvres2  33551  cycpmco2lem6  33571  cycpmconjvlem  33581  cycpmconjslem2  33595  elrgspnsubrunlem2  33688  fldgenssv  33756  fldgenssp  33759  nsgmgc  33841  idlsrgmulrss1  33921  idlsrgmulrss2  33922  esplyfval1  34083  esplyfvaln  34084  esplyind  34085  fedgmullem1  34139  fedgmullem2  34140  constrsscn  34250  constrmon  34254  ist0cld  34343  locfinreflem  34350  cmpcref  34360  zarcls0  34378  zarclsiin  34381  zarcmplem  34391  cnvordtrestixx  34423  ordtrestNEW  34431  ordtrest2NEW  34433  pnfneige0  34461  sigagenss  34660  imambfm  34773  dya2iocress  34785  dya2icoseg  34788  dya2iocucvr  34795  ballotlemro  35034  ftc2re  35106  bnj1097  35490  bnj1452  35561  rankscottu  35636  cvmlift3lem6  35903  msubrn  36108  mclsssv  36143  mclsind  36149  liness  36725  neibastop2lem  36979  ttcmin  37115  dfttc3gw  37142  opnmbllem0  38405  mblfinlem2  38407  isbndx  38532  isbnd2  38533  ssbnd  38538  heiborlem3  38563  igenmin  38814  lsatlss  39869  lsmsat  39881  lsatfixedN  39882  lssats  39885  lpssat  39886  lssatle  39888  lssat  39889  lsatcvat3  39925  paddssat  40687  paddasslem17  40709  pmodlem2  40720  hlmod1i  40729  pl42lem4N  40855  diassdvaN  41933  dia2dimlem10  41946  cdlemn4a  42072  cdlemn5pre  42073  dihord5apre  42135  lclkrlem2e  42384  lclkrlem2p  42395  lclkrlem2v  42401  lclkrslem2  42411  lclkrs  42412  lcfrlem25  42440  lcfrlem35  42450  mapdval2N  42503  mapdpglem8  42552  mapdpglem13  42557  baerlem3lem2  42583  mapdindp2  42594  hdmap11lem2  42715  primrootspoweq0  42972  aks6d1c6lem2  43037  evlsmhpvvval  43441  prjspnssbas  43467  elrfi  43539  isnacs3  43555  mzpf  43581  mzpindd  43591  diophrw  43604  eldiophss  43619  pw2f1ocnv  43878  aomclem6  43900  hbt  43971  oasubex  44127  oaabsb  44135  nnoeomeqom  44153  omcl2  44174  naddgeoa  44235  naddwordnexlem4  44242  oaltom  44245  omltoe  44247  minregex  44374  cnvssb  44426  trclubgNEW  44458  dfrcl2  44514  fvmptiunrelexplb0da  44525  relexp0a  44556  cotrcltrcl  44565  trclimalb2  44566  cotrclrcl  44582  isotone2  44889  k0004ss1  44991  fnresdmss  46000  mptelpm  46008  ssnnf1octb  46026  uzfissfz  46156  iuneqfzuzlem  46164  xlimliminflimsup  46690  icccncfext  46715  dvnprodlem2  46775  dvnprodlem3  46776  fourierdlem41  46976  fourierdlem70  47004  fourierdlem71  47005  fourierdlem80  47014  ioorrnopnlem  47132  ioorrnopnxrlem  47134  salgenss  47164  dfsalgen2  47169  subsaliuncllem  47185  iundjiun  47288  meadjiunlem  47293  meaiunlelem  47296  meaiuninclem  47308  meaiininclem  47314  omeunle  47344  carageniuncllem2  47350  caratheodorylem1  47354  caratheodorylem2  47355  hoissre  47372  ovnsubaddlem1  47398  hoidmvlelem3  47425  ovnhoilem1  47429  ovnhoilem2  47430  ovnhoi  47431  ovncvr2  47439  voncmpl  47449  hspmbllem2  47455  hspmbl  47457  opnvonmbllem1  47460  vonmblss  47468  ovnsubadd2lem  47473  vonioolem2  47509  preimaleiinlt  47549  issmfd  47563  issmfdf  47565  cnfsmf  47568  issmfled  47585  issmfgtd  47589  smfadd  47593  smfrec  47617  smfmul  47623  smfmulc1  47624  smfpimbor1lem2  47627  smfsuplem1  47639  smflimsuplem1  47648  smflimsuplem7  47654  tmachlem-uassst  47771  sprssspr  48381  isubgredgss  48781  isubgrsubgr  48785  uhgrimisgrgriclem  48846  stgrnbgr0  48880  uspgrlimlem3  48906  linc1  49355  iinfssc  49983  discsubc  49990  idfullsubc  50087