Theorem eqsstrd 3956

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  eqsstrrd  3957  eqsstrdi  3966  3sstr4d  3977  fpr2g  7166  tfisi  7810  suppssof1  8149  suppss2  8150  onfununi  8281  oawordeulem  8489  oeeui  8538  nnawordex  8573  oaabslem  8583  oaabs2  8585  omabslem  8586  omabs  8587  cofonr  8610  pw2f1olem  9019  fodomr  9066  fodomfir  9238  fival  9325  dffi3  9344  ordtypelem7  9439  ordtypelem8  9440  wemapso2lem  9467  cantnflt2  9594  cantnflem1  9610  tcss  9663  tcel  9664  r1val1  9710  rankuni2b  9777  tcrank  9808  cardonle  9881  harval2  9921  ackbij2  10164  cfub  10171  cflecard  10175  cfflb  10181  isf32lem8  10282  itunitc1  10342  ttukeylem7  10437  fpwwe2lem8  10561  wuncss  10668  wuncval2  10670  grur1a  10742  trclfvub  14969  cotrtrclfv  14974  relexpfld  15011  rtrclreclem4  15023  limsupgre  15443  isercolllem3  15629  4sqlem19  16934  vdwlem1  16952  vdwlem12  16963  ramub1lem1  16997  setsstruct2  17144  ressress  17217  imasaddfnlem  17492  imasaddflem  17494  imasvscafn  17501  imasvscaf  17503  imasless  17504  isohom  17743  ressffth  17907  acsfiindd  18519  acsmap2d  18521  dirref  18567  mndind  18796  f1omvdco2  19423  pmtrfrn  19433  symgsssg  19442  symggen  19445  psgnunilem1  19468  sylow2alem2  19593  lsmssv  19618  smndlsmidm  19631  gsumzres  19884  dprdlub  20003  dprdf1  20010  dprdsn  20013  dprdcntz2  20015  dprd2dlem1  20018  dprd2da  20019  dmdprdsplit2lem  20022  ablfac1eu  20050  rgspnmin  20592  drnglpir  21330  znleval  21534  evpmss  21566  frlmsplit2  21753  f1lindf  21802  issubassa2  21872  mplsubglem  21977  evlslem4  22054  evlseu  22061  mhpaddcl  22117  mhpinvcl  22118  psdmul  22132  lpsscls  23106  tgrest  23124  resttopon  23126  rest0  23134  restfpw  23144  ordtrest  23167  ordtrest2  23169  lmcnp  23269  tgcmp  23366  uncmp  23368  hauscmplem  23371  1stcfb  23410  2ndcdisj  23421  dissnref  23493  kgencmp  23510  xkouni  23564  prdstopn  23593  txtube  23605  txcmplem2  23607  xkoptsub  23619  xkopt  23620  xkococnlem  23624  qtoprest  23682  imastopn  23685  kqdisj  23697  reghmph  23758  nrmhmph  23759  fbssfi  23802  trfilss  23854  trfg  23856  elfm3  23915  alexsubALTlem3  24014  alexsubALT  24016  cnextf  24031  cnextcn  24032  clsnsg  24075  tgpconncompeqg  24077  qustgphaus  24088  trust  24194  ustuqtop3  24208  neipcfilu  24260  metequiv2  24475  prdsxmslem2  24494  metustfbas  24522  icccmplem1  24788  metdstri  24817  pi1addf  25014  pi1addval  25015  caubl  25275  caublcls  25276  relcmpcmet  25285  minveclem4  25399  hlhil  25410  ovolficcss  25436  uniioombllem3a  25551  uniioombllem3  25552  dyadss  25561  opnmbllem  25568  i1fima2  25646  limcfval  25839  dvfval  25864  dvnres  25898  dvivth  25977  lhop  25983  taylf  26326  xrlimcnp  26932  jensen  26952  ppisval  27067  chtlepsi  27169  chpub  27183  noextend  27630  nosupbday  27669  noinfbday  27684  cutsun12  27782  cutbdaybnd  27787  cutbdaybnd2  27788  cutbdaylt  27790  sltsbday  27909  cofcut1  27912  cofcutr  27916  addbday  28010  negbdaylem  28048  precsexlem8  28206  bdayons  28268  onsbnd2  28274  noseqind  28284  n0bday  28344  bdaypw2n0bndlem  28455  iscgrglt  28582  cyclnumvtx  29868  chssoc  31567  mdsl0  32381  mdexchi  32406  atcvat3i  32467  dmdbr5ati  32493  funimass4f  32710  xrofsup  32840  swrdrn2  33014  gsumpart  33124  pmtrcnel  33150  tocycfvres1  33171  tocycfvres2  33172  cycpmco2lem6  33192  cycpmconjvlem  33202  cycpmconjslem2  33216  elrgspnsubrunlem2  33309  fldgenssv  33376  fldgenssp  33379  nsgmgc  33472  idlsrgmulrss1  33571  idlsrgmulrss2  33572  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  fedgmullem1  33773  fedgmullem2  33774  constrsscn  33884  constrmon  33888  ist0cld  33977  locfinreflem  33984  cmpcref  33994  zarcls0  34012  zarclsiin  34015  zarcmplem  34025  cnvordtrestixx  34057  ordtrestNEW  34065  ordtrest2NEW  34067  pnfneige0  34095  sigagenss  34293  imambfm  34406  dya2iocress  34418  dya2icoseg  34421  dya2iocucvr  34428  ballotlemro  34667  ftc2re  34742  bnj1097  35123  bnj1452  35194  cvmlift3lem6  35506  msubrn  35711  mclsssv  35746  mclsind  35752  liness  36327  neibastop2lem  36542  ttcmin  36678  dfttc3gw  36705  opnmbllem0  37977  mblfinlem2  37979  isbndx  38103  isbnd2  38104  ssbnd  38109  heiborlem3  38134  igenmin  38385  lsatlss  39442  lsmsat  39454  lsatfixedN  39455  lssats  39458  lpssat  39459  lssatle  39461  lssat  39462  lsatcvat3  39498  paddssat  40260  paddasslem17  40282  pmodlem2  40293  hlmod1i  40302  pl42lem4N  40428  diassdvaN  41506  dia2dimlem10  41519  cdlemn4a  41645  cdlemn5pre  41646  dihord5apre  41708  lclkrlem2e  41957  lclkrlem2p  41968  lclkrlem2v  41974  lclkrslem2  41984  lclkrs  41985  lcfrlem25  42013  lcfrlem35  42023  mapdval2N  42076  mapdpglem8  42125  mapdpglem13  42130  baerlem3lem2  42156  mapdindp2  42167  hdmap11lem2  42288  primrootspoweq0  42545  aks6d1c6lem2  42610  evlsmhpvvval  43028  prjspnssbas  43054  elrfi  43126  isnacs3  43142  mzpf  43168  mzpindd  43178  diophrw  43191  eldiophss  43206  pw2f1ocnv  43465  aomclem6  43487  hbt  43558  oasubex  43714  oaabsb  43722  nnoeomeqom  43740  omcl2  43761  naddgeoa  43822  naddwordnexlem4  43829  oaltom  43832  omltoe  43834  minregex  43961  cnvssb  44013  trclubgNEW  44045  dfrcl2  44101  fvmptiunrelexplb0da  44112  relexp0a  44143  cotrcltrcl  44152  trclimalb2  44153  cotrclrcl  44169  isotone2  44476  k0004ss1  44578  fnresdmss  45598  mptelpm  45606  ssnnf1octb  45624  uzfissfz  45756  iuneqfzuzlem  45764  xlimliminflimsup  46290  icccncfext  46315  dvnprodlem2  46375  dvnprodlem3  46376  fourierdlem41  46576  fourierdlem70  46604  fourierdlem71  46605  fourierdlem80  46614  fourierdlem113  46647  ioorrnopnlem  46732  ioorrnopnxrlem  46734  salgenss  46764  dfsalgen2  46769  subsaliuncllem  46785  iundjiun  46888  meadjiunlem  46893  meaiunlelem  46896  meaiuninclem  46908  meaiininclem  46914  omeunle  46944  carageniuncllem2  46950  caratheodorylem1  46954  caratheodorylem2  46955  hoissre  46972  ovnsubaddlem1  46998  hoidmvlelem3  47025  ovnhoilem1  47029  ovnhoilem2  47030  ovnhoi  47031  ovncvr2  47039  voncmpl  47049  hspmbllem2  47055  hspmbl  47057  opnvonmbllem1  47060  vonmblss  47068  ovnsubadd2lem  47073  vonioolem2  47109  preimaleiinlt  47149  issmfd  47163  issmfdf  47165  sssmf  47166  cnfsmf  47168  issmfled  47185  issmfgtd  47189  smfadd  47193  smfrec  47217  smfmul  47223  smfmulc1  47224  smfpimbor1lem2  47227  smfsuplem1  47239  smflimsuplem1  47248  smflimsuplem7  47254  sprssspr  47941  isubgredgss  48341  isubgrsubgr  48345  uhgrimisgrgriclem  48406  stgrnbgr0  48440  uspgrlimlem3  48466  linc1  48901  iinfssc  49532  discsubc  49539  idfullsubc  49636