Theorem eqsstrd 3947

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqsstrrd  3948  eqsstrdi  3957  3sstr4d  3968  cnvssb  6207  fpr2g  7248  tfisi  7904  suppssof1  8254  suppss2  8255  onfununi  8387  oawordeulem  8600  oeeui  8649  nnawordex  8684  oaabslem  8694  oaabs2  8696  omabslem  8697  omabs  8698  cofonr  8721  pw2f1olem  9138  fodomr  9185  fodomfir  9357  fival  9441  dffi3  9460  ordtypelem7  9555  ordtypelem8  9556  wemapso2lem  9583  cantnflt2  9711  cantnflem1  9727  tcss  9780  tcel  9781  r1val1  9830  rankuni2b  9904  tcrank  9938  cardonle  10075  harval2  10117  ackbij2  10359  cfub  10365  cflecard  10369  cfflb  10376  isf32lem8  10477  itunitc1  10537  ttukeylem7  10632  fpwwe2lem8  10762  wuncss  10869  wuncval2  10871  grur1a  10943  trclfvub  15203  cotrtrclfv  15208  relexpfld  15245  rtrclreclem4  15257  limsupgre  15692  isercolllem3  15878  4sqlem19  17185  vdwlem1  17203  vdwlem12  17214  ramub1lem1  17248  setsstruct2  17396  ressress  17469  imasaddfnlem  17750  imasaddflem  17752  imasvscafn  17759  imasvscaf  17761  imasless  17762  isohom  18001  ressffth  18165  acsfiindd  18777  acsmap2d  18779  dirref  18825  mndind  19074  f1omvdco2  19713  pmtrfrn  19723  symgsssg  19732  symggen  19735  psgnunilem1  19758  sylow2alem2  19883  lsmssv  19908  smndlsmidm  19921  gsumzres  20174  dprdlub  20293  dprdf1  20300  dprdsn  20303  dprdcntz2  20305  dprd2dlem1  20308  dprd2da  20309  dmdprdsplit2lem  20312  ablfac1eu  20340  rgspnmin  20918  drnglpir  21707  znleval  21915  evpmss  21947  frlmsplit2  22134  f1lindf  22183  issubassa2  22255  mplsubglem  22361  evlslem4  22440  evlseu  22447  mhpaddcl  22527  mhpinvcl  22528  psdmul  22542  lpsscls  23514  tgrest  23532  resttopon  23534  rest0  23542  restfpw  23552  ordtrest  23575  ordtrest2  23577  lmcnp  23677  tgcmp  23774  uncmp  23776  hauscmplem  23779  1stcfb  23818  2ndcdisj  23830  dissnref  23902  kgencmp  23919  xkouni  23973  prdstopn  24002  txtube  24014  txcmplem2  24016  xkoptsub  24028  xkopt  24029  xkococnlem  24033  qtoprest  24091  imastopn  24094  kqdisj  24106  reghmph  24167  nrmhmph  24168  fbssfi  24211  trfilss  24263  trfg  24265  elfm3  24324  alexsubALTlem3  24423  alexsubALT  24425  cnextf  24440  cnextcn  24441  clsnsg  24484  tgpconncompeqg  24486  qustgphaus  24497  trust  24603  ustuqtop3  24617  neipcfilu  24669  metequiv2  24884  prdsxmslem2  24903  metustfbas  24931  icccmplem1  25197  metdstri  25226  pi1addf  25423  pi1addval  25424  caubl  25684  caublcls  25685  relcmpcmet  25694  minveclem4  25808  hlhil  25819  ovolficcss  25845  uniioombllem3a  25960  uniioombllem3  25961  dyadss  25970  opnmbllem  25977  i1fima2  26055  limcfval  26247  dvfval  26272  dvnres  26306  dvivth  26385  lhop  26391  taylf  26745  xrlimcnp  27353  jensen  27373  ppisval  27488  chtlepsi  27590  chpub  27604  noextend  28080  nosupbday  28119  noinfbday  28134  cutsun12  28233  cutbdaybnd  28238  cutbdaybnd2  28239  cutbdaylt  28241  sltsbday  28360  cofcut1  28363  cofcutr  28367  addbday  28461  negbdaylem  28499  precsexlem8  28657  bdayons  28719  onsbnd2  28725  noseqind  28735  n0bday  28795  bdaypw2n0bndlem  28906  iscgrglt  29034  cyclnumvtx  30445  chssoc  32155  mdsl0  32969  mdexchi  32994  atcvat3i  33055  dmdbr5ati  33081  funimass4f  33329  xrofsup  33455  swrdrn2  33613  gsumpart  33723  pmtrcnel  33749  tocycfvres1  33770  tocycfvres2  33771  cycpmco2lem6  33791  cycpmconjvlem  33801  cycpmconjslem2  33815  elrgspnsubrunlem2  33908  fldgenssv  33981  fldgenssp  33984  nsgmgc  34067  idlsrgmulrss1  34147  idlsrgmulrss2  34148  esplyfval1  34316  esplyfvaln  34317  esplyind  34318  fedgmullem1  34372  fedgmullem2  34373  constrsscn  34483  constrmon  34487  ist0cld  34576  locfinreflem  34583  cmpcref  34593  zarcls0  34611  zarclsiin  34614  zarcmplem  34624  cnvordtrestixx  34656  ordtrestNEW  34664  ordtrest2NEW  34666  pnfneige0  34694  sigagenss  34893  imambfm  35005  dya2iocress  35017  dya2icoseg  35020  dya2iocucvr  35027  ballotlemro  35266  ftc2re  35338  bnj1097  35722  bnj1452  35793  rankscottu  35880  cvmlift3lem6  36297  msubrn  36502  mclsssv  36537  mclsind  36543  liness  37125  neibastop2lem  37363  ttcmin  37499  dfttc3gw  37526  opnmbllem0  38842  mblfinlem2  38844  isbndx  38982  isbnd2  38983  ssbnd  38988  heiborlem3  39013  igenmin  39264  lsatlss  40319  lsmsat  40331  lsatfixedN  40332  lssats  40335  lpssat  40336  lssatle  40338  lssat  40339  lsatcvat3  40375  paddssat  41137  paddasslem17  41159  pmodlem2  41170  hlmod1i  41179  pl42lem4N  41305  diassdvaN  42383  dia2dimlem10  42396  cdlemn4a  42522  cdlemn5pre  42523  dihord5apre  42585  lclkrlem2e  42834  lclkrlem2p  42845  lclkrlem2v  42851  lclkrslem2  42861  lclkrs  42862  lcfrlem25  42890  lcfrlem35  42900  mapdval2N  42953  mapdpglem8  43002  mapdpglem13  43007  baerlem3lem2  43033  mapdindp2  43044  hdmap11lem2  43165  primrootspoweq0  43422  aks6d1c6lem2  43487  evlsmhpvvval  43889  prjspnssbas  43915  elrfi  43971  isnacs3  43987  mzpf  44013  mzpindd  44023  diophrw  44036  eldiophss  44051  pw2f1ocnv  44310  aomclem6  44327  hbt  44397  oasubex  44549  oaabsb  44557  nnoeomeqom  44575  omcl2  44596  naddgeoa  44657  naddwordnexlem4  44664  oaltom  44667  omltoe  44669  minregex  44796  trclubgNEW  44879  dfrcl2  44935  fvmptiunrelexplb0da  44946  relexp0a  44977  cotrcltrcl  44986  trclimalb2  44987  cotrclrcl  45003  isotone2  45310  k0004ss1  45412  fnresdmss  46456  mptelpm  46464  ssnnf1octb  46482  uzfissfz  46611  iuneqfzuzlem  46619  xlimliminflimsup  47145  icccncfext  47170  dvnprodlem2  47230  dvnprodlem3  47231  fourierdlem41  47431  fourierdlem70  47459  fourierdlem71  47460  fourierdlem80  47469  ioorrnopnlem  47587  ioorrnopnxrlem  47589  salgenss  47619  dfsalgen2  47624  subsaliuncllem  47640  iundjiun  47743  meadjiunlem  47748  meaiunlelem  47751  meaiuninclem  47763  meaiininclem  47769  omeunle  47799  carageniuncllem2  47805  caratheodorylem1  47809  caratheodorylem2  47810  hoissre  47827  ovnsubaddlem1  47853  hoidmvlelem3  47880  ovnhoilem1  47884  ovnhoilem2  47885  ovnhoi  47886  ovncvr2  47894  voncmpl  47904  hspmbllem2  47910  hspmbl  47912  opnvonmbllem1  47915  vonmblss  47923  ovnsubadd2lem  47928  vonioolem2  47964  preimaleiinlt  48004  issmfd  48018  issmfdf  48020  cnfsmf  48023  issmfled  48040  issmfgtd  48044  smfadd  48048  smfrec  48072  smfmul  48078  smfmulc1  48079  smfpimbor1lem2  48082  smfsuplem1  48094  smflimsuplem1  48103  smflimsuplem7  48109  tmachlem-uassst  48226  sprssspr  48836  isubgredgss  49236  isubgrsubgr  49240  uhgrimisgrgriclem  49301  stgrnbgr0  49335  uspgrlimlem3  49361  linc1  49868  iinfssc  50502  discsubc  50509  idfullsubc  50608