Theorem eqsstrd 3964

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  eqsstrrd  3965  eqsstrdi  3974  3sstr4d  3985  fpr2g  7140  tfisi  7784  suppssof1  8124  suppss2  8125  onfununi  8256  oawordeulem  8464  oeeui  8512  nnawordex  8547  oaabslem  8557  oaabs2  8559  omabslem  8560  omabs  8561  cofonr  8584  pw2f1olem  8989  fodomr  9036  fodomfir  9207  fival  9291  dffi3  9310  ordtypelem7  9405  ordtypelem8  9406  wemapso2lem  9433  cantnflt2  9558  cantnflem1  9574  tcss  9627  tcel  9628  r1val1  9674  rankuni2b  9741  tcrank  9772  cardonle  9845  harval2  9885  ackbij2  10128  cfub  10135  cflecard  10139  cfflb  10145  isf32lem8  10246  itunitc1  10306  ttukeylem7  10401  fpwwe2lem8  10524  wuncss  10631  wuncval2  10633  grur1a  10705  trclfvub  14909  cotrtrclfv  14914  relexpfld  14951  rtrclreclem4  14963  limsupgre  15383  isercolllem3  15569  4sqlem19  16870  vdwlem1  16888  vdwlem12  16899  ramub1lem1  16933  setsstruct2  17080  ressress  17153  imasaddfnlem  17427  imasaddflem  17429  imasvscafn  17436  imasvscaf  17438  imasless  17439  isohom  17678  ressffth  17842  acsfiindd  18454  acsmap2d  18456  dirref  18502  mndind  18731  f1omvdco2  19355  pmtrfrn  19365  symgsssg  19374  symggen  19377  psgnunilem1  19400  sylow2alem2  19525  lsmssv  19550  smndlsmidm  19563  gsumzres  19816  dprdlub  19935  dprdf1  19942  dprdsn  19945  dprdcntz2  19947  dprd2dlem1  19950  dprd2da  19951  dmdprdsplit2lem  19954  ablfac1eu  19982  rgspnmin  20525  drnglpir  21264  znleval  21486  evpmss  21518  frlmsplit2  21705  f1lindf  21754  issubassa2  21824  mplsubglem  21931  evlslem4  22006  evlseu  22013  mhpaddcl  22061  mhpinvcl  22062  psdmul  22076  lpsscls  23051  tgrest  23069  resttopon  23071  rest0  23079  restfpw  23089  ordtrest  23112  ordtrest2  23114  lmcnp  23214  tgcmp  23311  uncmp  23313  hauscmplem  23316  1stcfb  23355  2ndcdisj  23366  dissnref  23438  kgencmp  23455  xkouni  23509  prdstopn  23538  txtube  23550  txcmplem2  23552  xkoptsub  23564  xkopt  23565  xkococnlem  23569  qtoprest  23627  imastopn  23630  kqdisj  23642  reghmph  23703  nrmhmph  23704  fbssfi  23747  trfilss  23799  trfg  23801  elfm3  23860  alexsubALTlem3  23959  alexsubALT  23961  cnextf  23976  cnextcn  23977  clsnsg  24020  tgpconncompeqg  24022  qustgphaus  24033  trust  24139  ustuqtop3  24153  neipcfilu  24205  metequiv2  24420  prdsxmslem2  24439  metustfbas  24467  icccmplem1  24733  metdstri  24762  pi1addf  24969  pi1addval  24970  caubl  25230  caublcls  25231  relcmpcmet  25240  minveclem4  25354  hlhil  25365  ovolficcss  25392  uniioombllem3a  25507  uniioombllem3  25508  dyadss  25517  opnmbllem  25524  i1fima2  25602  limcfval  25795  dvfval  25820  dvnres  25855  dvivth  25937  lhop  25943  taylf  26290  xrlimcnp  26900  jensen  26921  ppisval  27036  chtlepsi  27139  chpub  27153  noextend  27600  nosupbday  27639  noinfbday  27654  scutun12  27746  scutbdaybnd  27751  scutbdaybnd2  27752  scutbdaylt  27754  cofcut1  27859  cofcutr  27863  addsbday  27955  negsbdaylem  27993  precsexlem8  28147  bdayon  28204  noseqind  28217  n0sbday  28275  iscgrglt  28487  cyclnumvtx  29773  chssoc  31468  mdsl0  32282  mdexchi  32307  atcvat3i  32368  dmdbr5ati  32394  funimass4f  32611  xrofsup  32742  swrdrn2  32927  gsumpart  33029  pmtrcnel  33050  tocycfvres1  33071  tocycfvres2  33072  cycpmco2lem6  33092  cycpmconjvlem  33102  cycpmconjslem2  33116  elrgspnsubrunlem2  33207  fldgenssv  33273  fldgenssp  33276  nsgmgc  33369  idlsrgmulrss1  33468  idlsrgmulrss2  33469  fedgmullem1  33634  fedgmullem2  33635  constrsscn  33745  constrmon  33749  ist0cld  33838  locfinreflem  33845  cmpcref  33855  zarcls0  33873  zarclsiin  33876  zarcmplem  33886  cnvordtrestixx  33918  ordtrestNEW  33926  ordtrest2NEW  33928  pnfneige0  33956  sigagenss  34154  imambfm  34267  dya2iocress  34279  dya2icoseg  34282  dya2iocucvr  34289  ballotlemro  34528  ftc2re  34603  bnj1097  34985  bnj1452  35056  cvmlift3lem6  35360  msubrn  35565  mclsssv  35600  mclsind  35606  liness  36179  neibastop2lem  36394  opnmbllem0  37696  mblfinlem2  37698  isbndx  37822  isbnd2  37823  ssbnd  37828  heiborlem3  37853  igenmin  38104  lsatlss  39035  lsmsat  39047  lsatfixedN  39048  lssats  39051  lpssat  39052  lssatle  39054  lssat  39055  lsatcvat3  39091  paddssat  39853  paddasslem17  39875  pmodlem2  39886  hlmod1i  39895  pl42lem4N  40021  diassdvaN  41099  dia2dimlem10  41112  cdlemn4a  41238  cdlemn5pre  41239  dihord5apre  41301  lclkrlem2e  41550  lclkrlem2p  41561  lclkrlem2v  41567  lclkrslem2  41577  lclkrs  41578  lcfrlem25  41606  lcfrlem35  41616  mapdval2N  41669  mapdpglem8  41718  mapdpglem13  41723  baerlem3lem2  41749  mapdindp2  41760  hdmap11lem2  41881  primrootspoweq0  42139  aks6d1c6lem2  42204  evlsmhpvvval  42628  prjspnssbas  42654  elrfi  42727  isnacs3  42743  mzpf  42769  mzpindd  42779  diophrw  42792  eldiophss  42807  pw2f1ocnv  43070  aomclem6  43092  hbt  43163  oasubex  43319  oaabsb  43327  nnoeomeqom  43345  omcl2  43366  naddgeoa  43427  naddwordnexlem4  43434  oaltom  43438  omltoe  43440  minregex  43567  cnvssb  43619  trclubgNEW  43651  dfrcl2  43707  fvmptiunrelexplb0da  43718  relexp0a  43749  cotrcltrcl  43758  trclimalb2  43759  cotrclrcl  43775  isotone2  44082  k0004ss1  44184  fnresdmss  45205  mptelpm  45213  ssnnf1octb  45231  uzfissfz  45365  iuneqfzuzlem  45373  xlimliminflimsup  45900  icccncfext  45925  dvnprodlem2  45985  dvnprodlem3  45986  fourierdlem41  46186  fourierdlem70  46214  fourierdlem71  46215  fourierdlem80  46224  fourierdlem113  46257  ioorrnopnlem  46342  ioorrnopnxrlem  46344  salgenss  46374  dfsalgen2  46379  subsaliuncllem  46395  iundjiun  46498  meadjiunlem  46503  meaiunlelem  46506  meaiuninclem  46518  meaiininclem  46524  omeunle  46554  carageniuncllem2  46560  caratheodorylem1  46564  caratheodorylem2  46565  hoissre  46582  ovnsubaddlem1  46608  hoidmvlelem3  46635  ovnhoilem1  46639  ovnhoilem2  46640  ovnhoi  46641  ovncvr2  46649  voncmpl  46659  hspmbllem2  46665  hspmbl  46667  opnvonmbllem1  46670  vonmblss  46678  ovnsubadd2lem  46683  vonioolem2  46719  preimageiingt  46758  preimaleiinlt  46759  issmfd  46773  issmfdf  46775  sssmf  46776  cnfsmf  46778  issmfled  46795  issmfgtd  46799  smfadd  46803  smfrec  46827  smfmul  46833  smfmulc1  46834  smfpimbor1lem2  46837  smfsuplem1  46849  smflimsuplem1  46858  smflimsuplem7  46864  sprssspr  47512  isubgredgss  47896  isubgrsubgr  47900  uhgrimisgrgriclem  47961  stgrnbgr0  47995  uspgrlimlem3  48021  linc1  48457  iinfssc  49089  discsubc  49096  idfullsubc  49193