Theorem eqsstrd 3943

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897

This theorem is used by:  eqsstrrd  3944  eqsstrdi  3953  3sstr4d  3964  cnvssb  6191  fpr2g  7221  tfisi  7874  suppssof1  8223  suppss2  8224  onfununi  8356  oawordeulem  8569  oeeui  8618  nnawordex  8653  oaabslem  8663  oaabs2  8665  omabslem  8666  omabs  8667  cofonr  8690  pw2f1olem  9107  fodomr  9154  fodomfir  9326  fival  9411  dffi3  9430  ordtypelem7  9525  ordtypelem8  9526  wemapso2lem  9553  cantnflt2  9681  cantnflem1  9697  tcss  9750  tcel  9751  r1val1  9800  rankuni2b  9874  tcrank  9908  cardonle  10045  harval2  10085  ackbij2  10327  cfub  10333  cflecard  10337  cfflb  10344  isf32lem8  10445  itunitc1  10505  ttukeylem7  10600  fpwwe2lem8  10730  wuncss  10837  wuncval2  10839  grur1a  10911  trclfvub  15169  cotrtrclfv  15174  relexpfld  15211  rtrclreclem4  15223  limsupgre  15657  isercolllem3  15843  4sqlem19  17150  vdwlem1  17168  vdwlem12  17179  ramub1lem1  17213  setsstruct2  17361  ressress  17434  imasaddfnlem  17709  imasaddflem  17711  imasvscafn  17718  imasvscaf  17720  imasless  17721  isohom  17960  ressffth  18124  acsfiindd  18736  acsmap2d  18738  dirref  18784  mndind  19033  f1omvdco2  19671  pmtrfrn  19681  symgsssg  19690  symggen  19693  psgnunilem1  19716  sylow2alem2  19841  lsmssv  19866  smndlsmidm  19879  gsumzres  20132  dprdlub  20251  dprdf1  20258  dprdsn  20261  dprdcntz2  20263  dprd2dlem1  20266  dprd2da  20267  dmdprdsplit2lem  20270  ablfac1eu  20298  rgspnmin  20876  drnglpir  21665  znleval  21869  evpmss  21901  frlmsplit2  22088  f1lindf  22137  issubassa2  22209  mplsubglem  22315  evlslem4  22394  evlseu  22401  mhpaddcl  22481  mhpinvcl  22482  psdmul  22496  lpsscls  23468  tgrest  23486  resttopon  23488  rest0  23496  restfpw  23506  ordtrest  23529  ordtrest2  23531  lmcnp  23631  tgcmp  23728  uncmp  23730  hauscmplem  23733  1stcfb  23772  2ndcdisj  23784  dissnref  23856  kgencmp  23873  xkouni  23927  prdstopn  23956  txtube  23968  txcmplem2  23970  xkoptsub  23982  xkopt  23983  xkococnlem  23987  qtoprest  24045  imastopn  24048  kqdisj  24060  reghmph  24121  nrmhmph  24122  fbssfi  24165  trfilss  24217  trfg  24219  elfm3  24278  alexsubALTlem3  24377  alexsubALT  24379  cnextf  24394  cnextcn  24395  clsnsg  24438  tgpconncompeqg  24440  qustgphaus  24451  trust  24557  ustuqtop3  24571  neipcfilu  24623  metequiv2  24838  prdsxmslem2  24857  metustfbas  24885  icccmplem1  25151  metdstri  25180  pi1addf  25377  pi1addval  25378  caubl  25638  caublcls  25639  relcmpcmet  25648  minveclem4  25762  hlhil  25773  ovolficcss  25799  uniioombllem3a  25914  uniioombllem3  25915  dyadss  25924  opnmbllem  25931  i1fima2  26009  limcfval  26201  dvfval  26226  dvnres  26260  dvivth  26339  lhop  26345  taylf  26697  xrlimcnp  27305  jensen  27325  ppisval  27440  chtlepsi  27542  chpub  27556  noextend  28032  nosupbday  28071  noinfbday  28086  cutsun12  28185  cutbdaybnd  28190  cutbdaybnd2  28191  cutbdaylt  28193  sltsbday  28312  cofcut1  28315  cofcutr  28319  addbday  28413  negbdaylem  28451  precsexlem8  28609  bdayons  28671  onsbnd2  28677  noseqind  28687  n0bday  28747  bdaypw2n0bndlem  28858  iscgrglt  28986  cyclnumvtx  30397  chssoc  32107  mdsl0  32921  mdexchi  32946  atcvat3i  33007  dmdbr5ati  33033  funimass4f  33282  xrofsup  33409  swrdrn2  33567  gsumpart  33674  pmtrcnel  33700  tocycfvres1  33721  tocycfvres2  33722  cycpmco2lem6  33742  cycpmconjvlem  33752  cycpmconjslem2  33766  elrgspnsubrunlem2  33859  fldgenssv  33927  fldgenssp  33930  nsgmgc  34013  idlsrgmulrss1  34093  idlsrgmulrss2  34094  esplyfval1  34255  esplyfvaln  34256  esplyind  34257  fedgmullem1  34311  fedgmullem2  34312  constrsscn  34422  constrmon  34426  ist0cld  34515  locfinreflem  34522  cmpcref  34532  zarcls0  34550  zarclsiin  34553  zarcmplem  34563  cnvordtrestixx  34595  ordtrestNEW  34603  ordtrest2NEW  34605  pnfneige0  34633  sigagenss  34832  imambfm  34944  dya2iocress  34956  dya2icoseg  34959  dya2iocucvr  34966  ballotlemro  35205  ftc2re  35277  bnj1097  35661  bnj1452  35732  rankscottu  35811  cvmlift3lem6  36179  msubrn  36384  mclsssv  36419  mclsind  36425  liness  37006  neibastop2lem  37244  ttcmin  37380  dfttc3gw  37407  opnmbllem0  38683  mblfinlem2  38685  isbndx  38825  isbnd2  38826  ssbnd  38831  heiborlem3  38856  igenmin  39107  lsatlss  40162  lsmsat  40174  lsatfixedN  40175  lssats  40178  lpssat  40179  lssatle  40181  lssat  40182  lsatcvat3  40218  paddssat  40980  paddasslem17  41002  pmodlem2  41013  hlmod1i  41022  pl42lem4N  41148  diassdvaN  42226  dia2dimlem10  42239  cdlemn4a  42365  cdlemn5pre  42366  dihord5apre  42428  lclkrlem2e  42677  lclkrlem2p  42688  lclkrlem2v  42694  lclkrslem2  42704  lclkrs  42705  lcfrlem25  42733  lcfrlem35  42743  mapdval2N  42796  mapdpglem8  42845  mapdpglem13  42850  baerlem3lem2  42876  mapdindp2  42887  hdmap11lem2  43008  primrootspoweq0  43265  aks6d1c6lem2  43330  evlsmhpvvval  43732  prjspnssbas  43758  elrfi  43814  isnacs3  43830  mzpf  43856  mzpindd  43866  diophrw  43879  eldiophss  43894  pw2f1ocnv  44153  aomclem6  44170  hbt  44241  oasubex  44397  oaabsb  44405  nnoeomeqom  44423  omcl2  44444  naddgeoa  44505  naddwordnexlem4  44512  oaltom  44515  omltoe  44517  minregex  44644  trclubgNEW  44727  dfrcl2  44783  fvmptiunrelexplb0da  44794  relexp0a  44825  cotrcltrcl  44834  trclimalb2  44835  cotrclrcl  44851  isotone2  45158  k0004ss1  45260  fnresdmss  46291  mptelpm  46299  ssnnf1octb  46317  uzfissfz  46446  iuneqfzuzlem  46454  xlimliminflimsup  46980  icccncfext  47005  dvnprodlem2  47065  dvnprodlem3  47066  fourierdlem41  47266  fourierdlem70  47294  fourierdlem71  47295  fourierdlem80  47304  ioorrnopnlem  47422  ioorrnopnxrlem  47424  salgenss  47454  dfsalgen2  47459  subsaliuncllem  47475  iundjiun  47578  meadjiunlem  47583  meaiunlelem  47586  meaiuninclem  47598  meaiininclem  47604  omeunle  47634  carageniuncllem2  47640  caratheodorylem1  47644  caratheodorylem2  47645  hoissre  47662  ovnsubaddlem1  47688  hoidmvlelem3  47715  ovnhoilem1  47719  ovnhoilem2  47720  ovnhoi  47721  ovncvr2  47729  voncmpl  47739  hspmbllem2  47745  hspmbl  47747  opnvonmbllem1  47750  vonmblss  47758  ovnsubadd2lem  47763  vonioolem2  47799  preimaleiinlt  47839  issmfd  47853  issmfdf  47855  cnfsmf  47858  issmfled  47875  issmfgtd  47879  smfadd  47883  smfrec  47907  smfmul  47913  smfmulc1  47914  smfpimbor1lem2  47917  smfsuplem1  47929  smflimsuplem1  47938  smflimsuplem7  47944  tmachlem-uassst  48061  sprssspr  48671  isubgredgss  49071  isubgrsubgr  49075  uhgrimisgrgriclem  49136  stgrnbgr0  49170  uspgrlimlem3  49196  linc1  49645  iinfssc  50279  discsubc  50286  idfullsubc  50385