Theorem eqsstrd 3963

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  eqsstrrd  3964  eqsstrdi  3979  fpr2g  7081  tfisi  7693  suppssof1  7999  suppss2  8000  onfununi  8156  oawordeulem  8361  oeeui  8409  nnawordex  8444  oaabslem  8451  oaabs2  8453  omabslem  8454  omabs  8455  pw2f1olem  8832  fodomr  8880  fival  9132  dffi3  9151  ordtypelem7  9244  ordtypelem8  9245  wemapso2lem  9272  cantnflt2  9392  cantnflem1  9408  trpredmintr  9461  tcss  9485  tcel  9486  r1val1  9528  rankuni2b  9595  tcrank  9626  cardonle  9699  harval2  9739  ackbij2  9983  cfub  9989  cflecard  9993  cfflb  9999  isf32lem8  10100  itunitc1  10160  ttukeylem7  10255  fpwwe2lem8  10378  wuncss  10485  wuncval2  10487  grur1a  10559  trclfvub  14699  cotrtrclfv  14704  relexpfld  14741  rtrclreclem4  14753  limsupgre  15171  isercolllem3  15359  4sqlem19  16645  vdwlem1  16663  vdwlem12  16674  ramub1lem1  16708  setsstruct2  16856  ressress  16939  imasaddfnlem  17220  imasaddflem  17222  imasvscafn  17229  imasvscaf  17231  imasless  17232  isohom  17469  ressffth  17635  acsfiindd  18252  acsmap2d  18254  dirref  18300  mndind  18447  f1omvdco2  19037  pmtrfrn  19047  symgsssg  19056  symggen  19059  psgnunilem1  19082  sylow2alem2  19204  lsmssv  19229  smndlsmidm  19242  lsmidmOLD  19250  gsumzres  19491  dprdlub  19610  dprdf1  19617  dprdsn  19620  dprdcntz2  19622  dprd2dlem1  19625  dprd2da  19626  dmdprdsplit2lem  19629  ablfac1eu  19657  drnglpir  20505  znleval  20743  evpmss  20772  frlmsplit2  20961  f1lindf  21010  issubassa2  21077  mplsubglem  21186  evlslem4  21265  evlseu  21274  mhpaddcl  21322  mhpinvcl  21323  lpsscls  22273  tgrest  22291  resttopon  22293  rest0  22301  restfpw  22311  ordtrest  22334  ordtrest2  22336  lmcnp  22436  tgcmp  22533  uncmp  22535  hauscmplem  22538  1stcfb  22577  2ndcdisj  22588  dissnref  22660  kgencmp  22677  xkouni  22731  prdstopn  22760  txtube  22772  txcmplem2  22774  xkoptsub  22786  xkopt  22787  xkococnlem  22791  qtoprest  22849  imastopn  22852  kqdisj  22864  reghmph  22925  nrmhmph  22926  fbssfi  22969  trfilss  23021  trfg  23023  elfm3  23082  alexsubALTlem3  23181  alexsubALT  23183  cnextf  23198  cnextcn  23199  clsnsg  23242  tgpconncompeqg  23244  qustgphaus  23255  trust  23362  ustuqtop3  23376  neipcfilu  23429  metequiv2  23647  prdsxmslem2  23666  metustfbas  23694  icccmplem1  23966  metdstri  23995  pi1addf  24191  pi1addval  24192  caubl  24453  caublcls  24454  relcmpcmet  24463  minveclem4  24577  hlhil  24588  ovolficcss  24614  uniioombllem3a  24729  uniioombllem3  24730  dyadss  24739  opnmbllem  24746  i1fima2  24824  limcfval  25017  dvfval  25042  dvnres  25076  dvivth  25155  lhop  25161  taylf  25501  xrlimcnp  26099  jensen  26119  ppisval  26234  chtlepsi  26335  chpub  26349  iscgrglt  26856  chssoc  29837  mdsl0  30651  mdexchi  30676  atcvat3i  30737  dmdbr5ati  30763  funimass4f  30951  xrofsup  31069  swrdrn2  31205  gsumpart  31294  pmtrcnel  31337  tocycfvres1  31356  tocycfvres2  31357  cycpmco2lem6  31377  cycpmconjvlem  31387  cycpmconjslem2  31401  nsgmgc  31576  idlsrgmulrss1  31635  idlsrgmulrss2  31636  fedgmullem1  31689  fedgmullem2  31690  ist0cld  31762  locfinreflem  31769  cmpcref  31779  zarcls0  31797  zarclsiin  31800  zarcmplem  31810  cnvordtrestixx  31842  ordtrestNEW  31850  ordtrest2NEW  31852  pnfneige0  31880  sigagenss  32096  imambfm  32208  dya2iocress  32220  dya2icoseg  32223  dya2iocucvr  32230  ballotlemro  32468  ftc2re  32557  bnj1097  32940  bnj1452  33011  cvmlift3lem6  33265  msubrn  33470  mclsssv  33505  mclsind  33511  noextend  33848  nosupbday  33887  noinfbday  33902  scutun12  33983  scutbdaybnd  33988  scutbdaybnd2  33989  scutbdaylt  33991  cofcut1  34069  cofcutr  34071  liness  34426  neibastop2lem  34528  opnmbllem0  35792  mblfinlem2  35794  isbndx  35919  isbnd2  35920  ssbnd  35925  heiborlem3  35950  igenmin  36201  lsatlss  36989  lsmsat  37001  lsatfixedN  37002  lssats  37005  lpssat  37006  lssatle  37008  lssat  37009  lsatcvat3  37045  paddssat  37807  paddasslem17  37829  pmodlem2  37840  hlmod1i  37849  pl42lem4N  37975  diassdvaN  39053  dia2dimlem10  39066  cdlemn4a  39192  cdlemn5pre  39193  dihord5apre  39255  lclkrlem2e  39504  lclkrlem2p  39515  lclkrlem2v  39521  lclkrslem2  39531  lclkrs  39532  lcfrlem25  39560  lcfrlem35  39570  mapdval2N  39623  mapdpglem8  39672  mapdpglem13  39677  baerlem3lem2  39703  mapdindp2  39714  hdmap11lem2  39835  elrfi  40496  isnacs3  40512  mzpf  40538  mzpindd  40548  diophrw  40561  eldiophss  40576  rmxyelqirr  40712  pw2f1ocnv  40839  aomclem6  40864  hbt  40935  rgspnmin  40976  cnvssb  41147  trclubgNEW  41179  dfrcl2  41235  fvmptiunrelexplb0da  41246  relexp0a  41277  cotrcltrcl  41286  trclimalb2  41287  cotrclrcl  41303  isotone2  41612  k0004ss1  41714  fnresdmss  42657  mptelpm  42665  ssnnf1octb  42686  uzfissfz  42819  iuneqfzuzlem  42827  xlimliminflimsup  43357  icccncfext  43382  dvnprodlem1  43441  dvnprodlem2  43442  dvnprodlem3  43443  fourierdlem41  43643  fourierdlem70  43671  fourierdlem71  43672  fourierdlem80  43681  fourierdlem113  43714  ioorrnopnlem  43799  ioorrnopnxrlem  43801  salgenss  43829  dfsalgen2  43834  subsaliuncllem  43850  iundjiun  43952  meadjiunlem  43957  meaiunlelem  43960  meaiuninclem  43972  meaiininclem  43978  omeunle  44008  carageniuncllem2  44014  caratheodorylem1  44018  caratheodorylem2  44019  hoissre  44036  ovnsubaddlem1  44062  hoidmvlelem3  44089  ovnhoilem1  44093  ovnhoilem2  44094  ovnhoi  44095  ovncvr2  44103  voncmpl  44113  hspmbllem2  44119  hspmbl  44121  opnvonmbllem1  44124  vonmblss  44132  ovnsubadd2lem  44137  vonioolem2  44173  preimageiingt  44208  preimaleiinlt  44209  issmfd  44222  issmfdf  44224  sssmf  44225  cnfsmf  44227  issmfled  44244  issmfgtd  44247  smfadd  44251  smfrec  44274  smfmul  44280  smfmulc1  44281  smfpimbor1lem2  44284  smfsuplem1  44295  smflimsuplem1  44304  smflimsuplem7  44310  sprssspr  44885  linc1  45718