Theorem eqsstrd 3981

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  eqsstrrd  3982  eqsstrdi  3991  3sstr4d  4002  fpr2g  7185  tfisi  7835  suppssof1  8178  suppss2  8179  onfununi  8310  oawordeulem  8518  oeeui  8566  nnawordex  8601  oaabslem  8611  oaabs2  8613  omabslem  8614  omabs  8615  cofonr  8638  pw2f1olem  9045  fodomr  9092  fodomfir  9279  fival  9363  dffi3  9382  ordtypelem7  9477  ordtypelem8  9478  wemapso2lem  9505  cantnflt2  9626  cantnflem1  9642  tcss  9697  tcel  9698  r1val1  9739  rankuni2b  9806  tcrank  9837  cardonle  9910  harval2  9950  ackbij2  10195  cfub  10202  cflecard  10206  cfflb  10212  isf32lem8  10313  itunitc1  10373  ttukeylem7  10468  fpwwe2lem8  10591  wuncss  10698  wuncval2  10700  grur1a  10772  trclfvub  14973  cotrtrclfv  14978  relexpfld  15015  rtrclreclem4  15027  limsupgre  15447  isercolllem3  15633  4sqlem19  16934  vdwlem1  16952  vdwlem12  16963  ramub1lem1  16997  setsstruct2  17144  ressress  17217  imasaddfnlem  17491  imasaddflem  17493  imasvscafn  17500  imasvscaf  17502  imasless  17503  isohom  17738  ressffth  17902  acsfiindd  18512  acsmap2d  18514  dirref  18560  mndind  18755  f1omvdco2  19378  pmtrfrn  19388  symgsssg  19397  symggen  19400  psgnunilem1  19423  sylow2alem2  19548  lsmssv  19573  smndlsmidm  19586  gsumzres  19839  dprdlub  19958  dprdf1  19965  dprdsn  19968  dprdcntz2  19970  dprd2dlem1  19973  dprd2da  19974  dmdprdsplit2lem  19977  ablfac1eu  20005  rgspnmin  20524  drnglpir  21242  znleval  21464  evpmss  21495  frlmsplit2  21682  f1lindf  21731  issubassa2  21801  mplsubglem  21908  evlslem4  21983  evlseu  21990  mhpaddcl  22038  mhpinvcl  22039  psdmul  22053  lpsscls  23028  tgrest  23046  resttopon  23048  rest0  23056  restfpw  23066  ordtrest  23089  ordtrest2  23091  lmcnp  23191  tgcmp  23288  uncmp  23290  hauscmplem  23293  1stcfb  23332  2ndcdisj  23343  dissnref  23415  kgencmp  23432  xkouni  23486  prdstopn  23515  txtube  23527  txcmplem2  23529  xkoptsub  23541  xkopt  23542  xkococnlem  23546  qtoprest  23604  imastopn  23607  kqdisj  23619  reghmph  23680  nrmhmph  23681  fbssfi  23724  trfilss  23776  trfg  23778  elfm3  23837  alexsubALTlem3  23936  alexsubALT  23938  cnextf  23953  cnextcn  23954  clsnsg  23997  tgpconncompeqg  23999  qustgphaus  24010  trust  24117  ustuqtop3  24131  neipcfilu  24183  metequiv2  24398  prdsxmslem2  24417  metustfbas  24445  icccmplem1  24711  metdstri  24740  pi1addf  24947  pi1addval  24948  caubl  25208  caublcls  25209  relcmpcmet  25218  minveclem4  25332  hlhil  25343  ovolficcss  25370  uniioombllem3a  25485  uniioombllem3  25486  dyadss  25495  opnmbllem  25502  i1fima2  25580  limcfval  25773  dvfval  25798  dvnres  25833  dvivth  25915  lhop  25921  taylf  26268  xrlimcnp  26878  jensen  26899  ppisval  27014  chtlepsi  27117  chpub  27131  noextend  27578  nosupbday  27617  noinfbday  27632  scutun12  27722  scutbdaybnd  27727  scutbdaybnd2  27728  scutbdaylt  27730  cofcut1  27828  cofcutr  27832  addsbday  27924  negsbdaylem  27962  precsexlem8  28116  bdayon  28173  noseqind  28186  n0sbday  28244  iscgrglt  28441  cyclnumvtx  29730  chssoc  31425  mdsl0  32239  mdexchi  32264  atcvat3i  32325  dmdbr5ati  32351  funimass4f  32561  xrofsup  32690  swrdrn2  32876  gsumpart  32997  pmtrcnel  33046  tocycfvres1  33067  tocycfvres2  33068  cycpmco2lem6  33088  cycpmconjvlem  33098  cycpmconjslem2  33112  elrgspnsubrunlem2  33199  fldgenssv  33265  fldgenssp  33268  nsgmgc  33383  idlsrgmulrss1  33482  idlsrgmulrss2  33483  fedgmullem1  33625  fedgmullem2  33626  constrsscn  33730  constrmon  33734  ist0cld  33823  locfinreflem  33830  cmpcref  33840  zarcls0  33858  zarclsiin  33861  zarcmplem  33871  cnvordtrestixx  33903  ordtrestNEW  33911  ordtrest2NEW  33913  pnfneige0  33941  sigagenss  34139  imambfm  34253  dya2iocress  34265  dya2icoseg  34268  dya2iocucvr  34275  ballotlemro  34514  ftc2re  34589  bnj1097  34971  bnj1452  35042  cvmlift3lem6  35311  msubrn  35516  mclsssv  35551  mclsind  35557  liness  36133  neibastop2lem  36348  opnmbllem0  37650  mblfinlem2  37652  isbndx  37776  isbnd2  37777  ssbnd  37782  heiborlem3  37807  igenmin  38058  lsatlss  38989  lsmsat  39001  lsatfixedN  39002  lssats  39005  lpssat  39006  lssatle  39008  lssat  39009  lsatcvat3  39045  paddssat  39808  paddasslem17  39830  pmodlem2  39841  hlmod1i  39850  pl42lem4N  39976  diassdvaN  41054  dia2dimlem10  41067  cdlemn4a  41193  cdlemn5pre  41194  dihord5apre  41256  lclkrlem2e  41505  lclkrlem2p  41516  lclkrlem2v  41522  lclkrslem2  41532  lclkrs  41533  lcfrlem25  41561  lcfrlem35  41571  mapdval2N  41624  mapdpglem8  41673  mapdpglem13  41678  baerlem3lem2  41704  mapdindp2  41715  hdmap11lem2  41836  primrootspoweq0  42094  aks6d1c6lem2  42159  evlsmhpvvval  42583  prjspnssbas  42609  elrfi  42682  isnacs3  42698  mzpf  42724  mzpindd  42734  diophrw  42747  eldiophss  42762  rmxyelqirrOLD  42899  pw2f1ocnv  43026  aomclem6  43048  hbt  43119  oasubex  43275  oaabsb  43283  nnoeomeqom  43301  omcl2  43322  naddgeoa  43383  naddwordnexlem4  43390  oaltom  43394  omltoe  43396  minregex  43523  cnvssb  43575  trclubgNEW  43607  dfrcl2  43663  fvmptiunrelexplb0da  43674  relexp0a  43705  cotrcltrcl  43714  trclimalb2  43715  cotrclrcl  43731  isotone2  44038  k0004ss1  44140  fnresdmss  45162  mptelpm  45170  ssnnf1octb  45188  uzfissfz  45322  iuneqfzuzlem  45330  xlimliminflimsup  45860  icccncfext  45885  dvnprodlem2  45945  dvnprodlem3  45946  fourierdlem41  46146  fourierdlem70  46174  fourierdlem71  46175  fourierdlem80  46184  fourierdlem113  46217  ioorrnopnlem  46302  ioorrnopnxrlem  46304  salgenss  46334  dfsalgen2  46339  subsaliuncllem  46355  iundjiun  46458  meadjiunlem  46463  meaiunlelem  46466  meaiuninclem  46478  meaiininclem  46484  omeunle  46514  carageniuncllem2  46520  caratheodorylem1  46524  caratheodorylem2  46525  hoissre  46542  ovnsubaddlem1  46568  hoidmvlelem3  46595  ovnhoilem1  46599  ovnhoilem2  46600  ovnhoi  46601  ovncvr2  46609  voncmpl  46619  hspmbllem2  46625  hspmbl  46627  opnvonmbllem1  46630  vonmblss  46638  ovnsubadd2lem  46643  vonioolem2  46679  preimageiingt  46718  preimaleiinlt  46719  issmfd  46733  issmfdf  46735  sssmf  46736  cnfsmf  46738  issmfled  46755  issmfgtd  46759  smfadd  46763  smfrec  46787  smfmul  46793  smfmulc1  46794  smfpimbor1lem2  46797  smfsuplem1  46809  smflimsuplem1  46818  smflimsuplem7  46824  sprssspr  47482  isubgredgss  47865  isubgrsubgr  47869  uhgrimisgrgriclem  47930  stgrnbgr0  47963  uspgrlimlem3  47989  linc1  48414  iinfssc  49046  discsubc  49053  idfullsubc  49150