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

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

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 2123  ax-ext 2705

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

This theorem is referenced by:  eqsstrrd  3966  eqsstrdi  3975  3sstr4d  3986  fpr2g  7154  tfisi  7798  suppssof1  8138  suppss2  8139  onfununi  8270  oawordeulem  8478  oeeui  8526  nnawordex  8561  oaabslem  8571  oaabs2  8573  omabslem  8574  omabs  8575  cofonr  8598  pw2f1olem  9005  fodomr  9052  fodomfir  9223  fival  9307  dffi3  9326  ordtypelem7  9421  ordtypelem8  9422  wemapso2lem  9449  cantnflt2  9574  cantnflem1  9590  tcss  9643  tcel  9644  r1val1  9690  rankuni2b  9757  tcrank  9788  cardonle  9861  harval2  9901  ackbij2  10144  cfub  10151  cflecard  10155  cfflb  10161  isf32lem8  10262  itunitc1  10322  ttukeylem7  10417  fpwwe2lem8  10540  wuncss  10647  wuncval2  10649  grur1a  10721  trclfvub  14921  cotrtrclfv  14926  relexpfld  14963  rtrclreclem4  14975  limsupgre  15395  isercolllem3  15581  4sqlem19  16882  vdwlem1  16900  vdwlem12  16911  ramub1lem1  16945  setsstruct2  17092  ressress  17165  imasaddfnlem  17440  imasaddflem  17442  imasvscafn  17449  imasvscaf  17451  imasless  17452  isohom  17691  ressffth  17855  acsfiindd  18467  acsmap2d  18469  dirref  18515  mndind  18744  f1omvdco2  19368  pmtrfrn  19378  symgsssg  19387  symggen  19390  psgnunilem1  19413  sylow2alem2  19538  lsmssv  19563  smndlsmidm  19576  gsumzres  19829  dprdlub  19948  dprdf1  19955  dprdsn  19958  dprdcntz2  19960  dprd2dlem1  19963  dprd2da  19964  dmdprdsplit2lem  19967  ablfac1eu  19995  rgspnmin  20539  drnglpir  21278  znleval  21500  evpmss  21532  frlmsplit2  21719  f1lindf  21768  issubassa2  21839  mplsubglem  21945  evlslem4  22022  evlseu  22029  mhpaddcl  22085  mhpinvcl  22086  psdmul  22100  lpsscls  23076  tgrest  23094  resttopon  23096  rest0  23104  restfpw  23114  ordtrest  23137  ordtrest2  23139  lmcnp  23239  tgcmp  23336  uncmp  23338  hauscmplem  23341  1stcfb  23380  2ndcdisj  23391  dissnref  23463  kgencmp  23480  xkouni  23534  prdstopn  23563  txtube  23575  txcmplem2  23577  xkoptsub  23589  xkopt  23590  xkococnlem  23594  qtoprest  23652  imastopn  23655  kqdisj  23667  reghmph  23728  nrmhmph  23729  fbssfi  23772  trfilss  23824  trfg  23826  elfm3  23885  alexsubALTlem3  23984  alexsubALT  23986  cnextf  24001  cnextcn  24002  clsnsg  24045  tgpconncompeqg  24047  qustgphaus  24058  trust  24164  ustuqtop3  24178  neipcfilu  24230  metequiv2  24445  prdsxmslem2  24464  metustfbas  24492  icccmplem1  24758  metdstri  24787  pi1addf  24994  pi1addval  24995  caubl  25255  caublcls  25256  relcmpcmet  25265  minveclem4  25379  hlhil  25390  ovolficcss  25417  uniioombllem3a  25532  uniioombllem3  25533  dyadss  25542  opnmbllem  25549  i1fima2  25627  limcfval  25820  dvfval  25845  dvnres  25880  dvivth  25962  lhop  25968  taylf  26315  xrlimcnp  26925  jensen  26946  ppisval  27061  chtlepsi  27164  chpub  27178  noextend  27625  nosupbday  27664  noinfbday  27679  scutun12  27771  scutbdaybnd  27776  scutbdaybnd2  27777  scutbdaylt  27779  cofcut1  27884  cofcutr  27888  addsbday  27980  negsbdaylem  28018  precsexlem8  28172  bdayon  28229  noseqind  28242  n0sbday  28300  iscgrglt  28512  cyclnumvtx  29799  chssoc  31497  mdsl0  32311  mdexchi  32336  atcvat3i  32397  dmdbr5ati  32423  funimass4f  32641  xrofsup  32775  swrdrn2  32964  gsumpart  33074  pmtrcnel  33099  tocycfvres1  33120  tocycfvres2  33121  cycpmco2lem6  33141  cycpmconjvlem  33151  cycpmconjslem2  33165  elrgspnsubrunlem2  33258  fldgenssv  33325  fldgenssp  33328  nsgmgc  33421  idlsrgmulrss1  33520  idlsrgmulrss2  33521  esplyind  33659  fedgmullem1  33714  fedgmullem2  33715  constrsscn  33825  constrmon  33829  ist0cld  33918  locfinreflem  33925  cmpcref  33935  zarcls0  33953  zarclsiin  33956  zarcmplem  33966  cnvordtrestixx  33998  ordtrestNEW  34006  ordtrest2NEW  34008  pnfneige0  34036  sigagenss  34234  imambfm  34347  dya2iocress  34359  dya2icoseg  34362  dya2iocucvr  34369  ballotlemro  34608  ftc2re  34683  bnj1097  35065  bnj1452  35136  cvmlift3lem6  35440  msubrn  35645  mclsssv  35680  mclsind  35686  liness  36261  neibastop2lem  36476  opnmbllem0  37769  mblfinlem2  37771  isbndx  37895  isbnd2  37896  ssbnd  37901  heiborlem3  37926  igenmin  38177  lsatlss  39168  lsmsat  39180  lsatfixedN  39181  lssats  39184  lpssat  39185  lssatle  39187  lssat  39188  lsatcvat3  39224  paddssat  39986  paddasslem17  40008  pmodlem2  40019  hlmod1i  40028  pl42lem4N  40154  diassdvaN  41232  dia2dimlem10  41245  cdlemn4a  41371  cdlemn5pre  41372  dihord5apre  41434  lclkrlem2e  41683  lclkrlem2p  41694  lclkrlem2v  41700  lclkrslem2  41710  lclkrs  41711  lcfrlem25  41739  lcfrlem35  41749  mapdval2N  41802  mapdpglem8  41851  mapdpglem13  41856  baerlem3lem2  41882  mapdindp2  41893  hdmap11lem2  42014  primrootspoweq0  42272  aks6d1c6lem2  42337  evlsmhpvvval  42753  prjspnssbas  42779  elrfi  42851  isnacs3  42867  mzpf  42893  mzpindd  42903  diophrw  42916  eldiophss  42931  pw2f1ocnv  43194  aomclem6  43216  hbt  43287  oasubex  43443  oaabsb  43451  nnoeomeqom  43469  omcl2  43490  naddgeoa  43551  naddwordnexlem4  43558  oaltom  43562  omltoe  43564  minregex  43691  cnvssb  43743  trclubgNEW  43775  dfrcl2  43831  fvmptiunrelexplb0da  43842  relexp0a  43873  cotrcltrcl  43882  trclimalb2  43883  cotrclrcl  43899  isotone2  44206  k0004ss1  44308  fnresdmss  45328  mptelpm  45336  ssnnf1octb  45354  uzfissfz  45487  iuneqfzuzlem  45495  xlimliminflimsup  46022  icccncfext  46047  dvnprodlem2  46107  dvnprodlem3  46108  fourierdlem41  46308  fourierdlem70  46336  fourierdlem71  46337  fourierdlem80  46346  fourierdlem113  46379  ioorrnopnlem  46464  ioorrnopnxrlem  46466  salgenss  46496  dfsalgen2  46501  subsaliuncllem  46517  iundjiun  46620  meadjiunlem  46625  meaiunlelem  46628  meaiuninclem  46640  meaiininclem  46646  omeunle  46676  carageniuncllem2  46682  caratheodorylem1  46686  caratheodorylem2  46687  hoissre  46704  ovnsubaddlem1  46730  hoidmvlelem3  46757  ovnhoilem1  46761  ovnhoilem2  46762  ovnhoi  46763  ovncvr2  46771  voncmpl  46781  hspmbllem2  46787  hspmbl  46789  opnvonmbllem1  46792  vonmblss  46800  ovnsubadd2lem  46805  vonioolem2  46841  preimaleiinlt  46881  issmfd  46895  issmfdf  46897  sssmf  46898  cnfsmf  46900  issmfled  46917  issmfgtd  46921  smfadd  46925  smfrec  46949  smfmul  46955  smfmulc1  46956  smfpimbor1lem2  46959  smfsuplem1  46971  smflimsuplem1  46980  smflimsuplem7  46986  sprssspr  47643  isubgredgss  48027  isubgrsubgr  48031  uhgrimisgrgriclem  48092  stgrnbgr0  48126  uspgrlimlem3  48152  linc1  48587  iinfssc  49218  discsubc  49225  idfullsubc  49322