Theorem eqsstrd 3984

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

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

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 2702

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

This theorem is referenced by:  eqsstrrd  3985  eqsstrdi  3994  3sstr4d  4005  fpr2g  7188  tfisi  7838  suppssof1  8181  suppss2  8182  onfununi  8313  oawordeulem  8521  oeeui  8569  nnawordex  8604  oaabslem  8614  oaabs2  8616  omabslem  8617  omabs  8618  cofonr  8641  pw2f1olem  9050  fodomr  9098  fodomfir  9286  fival  9370  dffi3  9389  ordtypelem7  9484  ordtypelem8  9485  wemapso2lem  9512  cantnflt2  9633  cantnflem1  9649  tcss  9704  tcel  9705  r1val1  9746  rankuni2b  9813  tcrank  9844  cardonle  9917  harval2  9957  ackbij2  10202  cfub  10209  cflecard  10213  cfflb  10219  isf32lem8  10320  itunitc1  10380  ttukeylem7  10475  fpwwe2lem8  10598  wuncss  10705  wuncval2  10707  grur1a  10779  trclfvub  14980  cotrtrclfv  14985  relexpfld  15022  rtrclreclem4  15034  limsupgre  15454  isercolllem3  15640  4sqlem19  16941  vdwlem1  16959  vdwlem12  16970  ramub1lem1  17004  setsstruct2  17151  ressress  17224  imasaddfnlem  17498  imasaddflem  17500  imasvscafn  17507  imasvscaf  17509  imasless  17510  isohom  17745  ressffth  17909  acsfiindd  18519  acsmap2d  18521  dirref  18567  mndind  18762  f1omvdco2  19385  pmtrfrn  19395  symgsssg  19404  symggen  19407  psgnunilem1  19430  sylow2alem2  19555  lsmssv  19580  smndlsmidm  19593  gsumzres  19846  dprdlub  19965  dprdf1  19972  dprdsn  19975  dprdcntz2  19977  dprd2dlem1  19980  dprd2da  19981  dmdprdsplit2lem  19984  ablfac1eu  20012  rgspnmin  20531  drnglpir  21249  znleval  21471  evpmss  21502  frlmsplit2  21689  f1lindf  21738  issubassa2  21808  mplsubglem  21915  evlslem4  21990  evlseu  21997  mhpaddcl  22045  mhpinvcl  22046  psdmul  22060  lpsscls  23035  tgrest  23053  resttopon  23055  rest0  23063  restfpw  23073  ordtrest  23096  ordtrest2  23098  lmcnp  23198  tgcmp  23295  uncmp  23297  hauscmplem  23300  1stcfb  23339  2ndcdisj  23350  dissnref  23422  kgencmp  23439  xkouni  23493  prdstopn  23522  txtube  23534  txcmplem2  23536  xkoptsub  23548  xkopt  23549  xkococnlem  23553  qtoprest  23611  imastopn  23614  kqdisj  23626  reghmph  23687  nrmhmph  23688  fbssfi  23731  trfilss  23783  trfg  23785  elfm3  23844  alexsubALTlem3  23943  alexsubALT  23945  cnextf  23960  cnextcn  23961  clsnsg  24004  tgpconncompeqg  24006  qustgphaus  24017  trust  24124  ustuqtop3  24138  neipcfilu  24190  metequiv2  24405  prdsxmslem2  24424  metustfbas  24452  icccmplem1  24718  metdstri  24747  pi1addf  24954  pi1addval  24955  caubl  25215  caublcls  25216  relcmpcmet  25225  minveclem4  25339  hlhil  25350  ovolficcss  25377  uniioombllem3a  25492  uniioombllem3  25493  dyadss  25502  opnmbllem  25509  i1fima2  25587  limcfval  25780  dvfval  25805  dvnres  25840  dvivth  25922  lhop  25928  taylf  26275  xrlimcnp  26885  jensen  26906  ppisval  27021  chtlepsi  27124  chpub  27138  noextend  27585  nosupbday  27624  noinfbday  27639  scutun12  27729  scutbdaybnd  27734  scutbdaybnd2  27735  scutbdaylt  27737  cofcut1  27835  cofcutr  27839  addsbday  27931  negsbdaylem  27969  precsexlem8  28123  bdayon  28180  noseqind  28193  n0sbday  28251  iscgrglt  28448  cyclnumvtx  29737  chssoc  31432  mdsl0  32246  mdexchi  32271  atcvat3i  32332  dmdbr5ati  32358  funimass4f  32568  xrofsup  32697  swrdrn2  32883  gsumpart  33004  pmtrcnel  33053  tocycfvres1  33074  tocycfvres2  33075  cycpmco2lem6  33095  cycpmconjvlem  33105  cycpmconjslem2  33119  elrgspnsubrunlem2  33206  fldgenssv  33272  fldgenssp  33275  nsgmgc  33390  idlsrgmulrss1  33489  idlsrgmulrss2  33490  fedgmullem1  33632  fedgmullem2  33633  constrsscn  33737  constrmon  33741  ist0cld  33830  locfinreflem  33837  cmpcref  33847  zarcls0  33865  zarclsiin  33868  zarcmplem  33878  cnvordtrestixx  33910  ordtrestNEW  33918  ordtrest2NEW  33920  pnfneige0  33948  sigagenss  34146  imambfm  34260  dya2iocress  34272  dya2icoseg  34275  dya2iocucvr  34282  ballotlemro  34521  ftc2re  34596  bnj1097  34978  bnj1452  35049  cvmlift3lem6  35318  msubrn  35523  mclsssv  35558  mclsind  35564  liness  36140  neibastop2lem  36355  opnmbllem0  37657  mblfinlem2  37659  isbndx  37783  isbnd2  37784  ssbnd  37789  heiborlem3  37814  igenmin  38065  lsatlss  38996  lsmsat  39008  lsatfixedN  39009  lssats  39012  lpssat  39013  lssatle  39015  lssat  39016  lsatcvat3  39052  paddssat  39815  paddasslem17  39837  pmodlem2  39848  hlmod1i  39857  pl42lem4N  39983  diassdvaN  41061  dia2dimlem10  41074  cdlemn4a  41200  cdlemn5pre  41201  dihord5apre  41263  lclkrlem2e  41512  lclkrlem2p  41523  lclkrlem2v  41529  lclkrslem2  41539  lclkrs  41540  lcfrlem25  41568  lcfrlem35  41578  mapdval2N  41631  mapdpglem8  41680  mapdpglem13  41685  baerlem3lem2  41711  mapdindp2  41722  hdmap11lem2  41843  primrootspoweq0  42101  aks6d1c6lem2  42166  evlsmhpvvval  42590  prjspnssbas  42616  elrfi  42689  isnacs3  42705  mzpf  42731  mzpindd  42741  diophrw  42754  eldiophss  42769  rmxyelqirrOLD  42906  pw2f1ocnv  43033  aomclem6  43055  hbt  43126  oasubex  43282  oaabsb  43290  nnoeomeqom  43308  omcl2  43329  naddgeoa  43390  naddwordnexlem4  43397  oaltom  43401  omltoe  43403  minregex  43530  cnvssb  43582  trclubgNEW  43614  dfrcl2  43670  fvmptiunrelexplb0da  43681  relexp0a  43712  cotrcltrcl  43721  trclimalb2  43722  cotrclrcl  43738  isotone2  44045  k0004ss1  44147  fnresdmss  45169  mptelpm  45177  ssnnf1octb  45195  uzfissfz  45329  iuneqfzuzlem  45337  xlimliminflimsup  45867  icccncfext  45892  dvnprodlem2  45952  dvnprodlem3  45953  fourierdlem41  46153  fourierdlem70  46181  fourierdlem71  46182  fourierdlem80  46191  fourierdlem113  46224  ioorrnopnlem  46309  ioorrnopnxrlem  46311  salgenss  46341  dfsalgen2  46346  subsaliuncllem  46362  iundjiun  46465  meadjiunlem  46470  meaiunlelem  46473  meaiuninclem  46485  meaiininclem  46491  omeunle  46521  carageniuncllem2  46527  caratheodorylem1  46531  caratheodorylem2  46532  hoissre  46549  ovnsubaddlem1  46575  hoidmvlelem3  46602  ovnhoilem1  46606  ovnhoilem2  46607  ovnhoi  46608  ovncvr2  46616  voncmpl  46626  hspmbllem2  46632  hspmbl  46634  opnvonmbllem1  46637  vonmblss  46645  ovnsubadd2lem  46650  vonioolem2  46686  preimageiingt  46725  preimaleiinlt  46726  issmfd  46740  issmfdf  46742  sssmf  46743  cnfsmf  46745  issmfled  46762  issmfgtd  46766  smfadd  46770  smfrec  46794  smfmul  46800  smfmulc1  46801  smfpimbor1lem2  46804  smfsuplem1  46816  smflimsuplem1  46825  smflimsuplem7  46831  sprssspr  47486  isubgredgss  47869  isubgrsubgr  47873  uhgrimisgrgriclem  47934  stgrnbgr0  47967  uspgrlimlem3  47993  linc1  48418  iinfssc  49050  discsubc  49057  idfullsubc  49154