Theorem eqsstrd 4047

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqsstrrd  4048  eqsstrdi  4063  fpr2g  7248  tfisi  7896  suppssof1  8240  suppss2  8241  onfununi  8397  oawordeulem  8610  oeeui  8658  nnawordex  8693  oaabslem  8703  oaabs2  8705  omabslem  8706  omabs  8707  cofonr  8730  pw2f1olem  9142  fodomr  9194  fodomfir  9396  fival  9481  dffi3  9500  ordtypelem7  9593  ordtypelem8  9594  wemapso2lem  9621  cantnflt2  9742  cantnflem1  9758  tcss  9813  tcel  9814  r1val1  9855  rankuni2b  9922  tcrank  9953  cardonle  10026  harval2  10066  ackbij2  10311  cfub  10318  cflecard  10322  cfflb  10328  isf32lem8  10429  itunitc1  10489  ttukeylem7  10584  fpwwe2lem8  10707  wuncss  10814  wuncval2  10816  grur1a  10888  trclfvub  15056  cotrtrclfv  15061  relexpfld  15098  rtrclreclem4  15110  limsupgre  15527  isercolllem3  15715  4sqlem19  17010  vdwlem1  17028  vdwlem12  17039  ramub1lem1  17073  setsstruct2  17221  ressress  17307  imasaddfnlem  17588  imasaddflem  17590  imasvscafn  17597  imasvscaf  17599  imasless  17600  isohom  17837  ressffth  18005  acsfiindd  18623  acsmap2d  18625  dirref  18671  mndind  18863  f1omvdco2  19490  pmtrfrn  19500  symgsssg  19509  symggen  19512  psgnunilem1  19535  sylow2alem2  19660  lsmssv  19685  smndlsmidm  19698  gsumzres  19951  dprdlub  20070  dprdf1  20077  dprdsn  20080  dprdcntz2  20082  dprd2dlem1  20085  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1eu  20117  drnglpir  21365  znleval  21596  evpmss  21627  frlmsplit2  21816  f1lindf  21865  issubassa2  21935  mplsubglem  22042  evlslem4  22123  evlseu  22130  mhpaddcl  22178  mhpinvcl  22179  psdmul  22193  lpsscls  23170  tgrest  23188  resttopon  23190  rest0  23198  restfpw  23208  ordtrest  23231  ordtrest2  23233  lmcnp  23333  tgcmp  23430  uncmp  23432  hauscmplem  23435  1stcfb  23474  2ndcdisj  23485  dissnref  23557  kgencmp  23574  xkouni  23628  prdstopn  23657  txtube  23669  txcmplem2  23671  xkoptsub  23683  xkopt  23684  xkococnlem  23688  qtoprest  23746  imastopn  23749  kqdisj  23761  reghmph  23822  nrmhmph  23823  fbssfi  23866  trfilss  23918  trfg  23920  elfm3  23979  alexsubALTlem3  24078  alexsubALT  24080  cnextf  24095  cnextcn  24096  clsnsg  24139  tgpconncompeqg  24141  qustgphaus  24152  trust  24259  ustuqtop3  24273  neipcfilu  24326  metequiv2  24544  prdsxmslem2  24563  metustfbas  24591  icccmplem1  24863  metdstri  24892  pi1addf  25099  pi1addval  25100  caubl  25361  caublcls  25362  relcmpcmet  25371  minveclem4  25485  hlhil  25496  ovolficcss  25523  uniioombllem3a  25638  uniioombllem3  25639  dyadss  25648  opnmbllem  25655  i1fima2  25733  limcfval  25927  dvfval  25952  dvnres  25987  dvivth  26069  lhop  26075  taylf  26420  xrlimcnp  27029  jensen  27050  ppisval  27165  chtlepsi  27268  chpub  27282  noextend  27729  nosupbday  27768  noinfbday  27783  scutun12  27873  scutbdaybnd  27878  scutbdaybnd2  27879  scutbdaylt  27881  cofcut1  27972  cofcutr  27976  addsbday  28068  negsbdaylem  28106  precsexlem8  28256  noseqind  28316  n0sbday  28372  pw2bday  28436  iscgrglt  28540  chssoc  31528  mdsl0  32342  mdexchi  32367  atcvat3i  32428  dmdbr5ati  32454  funimass4f  32656  xrofsup  32774  swrdrn2  32921  gsumpart  33038  pmtrcnel  33082  tocycfvres1  33103  tocycfvres2  33104  cycpmco2lem6  33124  cycpmconjvlem  33134  cycpmconjslem2  33148  fldgenssv  33282  fldgenssp  33285  nsgmgc  33405  idlsrgmulrss1  33504  idlsrgmulrss2  33505  fedgmullem1  33642  fedgmullem2  33643  constrsscn  33730  constrmon  33734  ist0cld  33779  locfinreflem  33786  cmpcref  33796  zarcls0  33814  zarclsiin  33817  zarcmplem  33827  cnvordtrestixx  33859  ordtrestNEW  33867  ordtrest2NEW  33869  pnfneige0  33897  sigagenss  34113  imambfm  34227  dya2iocress  34239  dya2icoseg  34242  dya2iocucvr  34249  ballotlemro  34487  ftc2re  34575  bnj1097  34957  bnj1452  35028  cvmlift3lem6  35292  msubrn  35497  mclsssv  35532  mclsind  35538  liness  36109  neibastop2lem  36326  opnmbllem0  37616  mblfinlem2  37618  isbndx  37742  isbnd2  37743  ssbnd  37748  heiborlem3  37773  igenmin  38024  lsatlss  38952  lsmsat  38964  lsatfixedN  38965  lssats  38968  lpssat  38969  lssatle  38971  lssat  38972  lsatcvat3  39008  paddssat  39771  paddasslem17  39793  pmodlem2  39804  hlmod1i  39813  pl42lem4N  39939  diassdvaN  41017  dia2dimlem10  41030  cdlemn4a  41156  cdlemn5pre  41157  dihord5apre  41219  lclkrlem2e  41468  lclkrlem2p  41479  lclkrlem2v  41485  lclkrslem2  41495  lclkrs  41496  lcfrlem25  41524  lcfrlem35  41534  mapdval2N  41587  mapdpglem8  41636  mapdpglem13  41641  baerlem3lem2  41667  mapdindp2  41678  hdmap11lem2  41799  primrootspoweq0  42063  aks6d1c6lem2  42128  evlsmhpvvval  42550  prjspnssbas  42576  elrfi  42650  isnacs3  42666  mzpf  42692  mzpindd  42702  diophrw  42715  eldiophss  42730  rmxyelqirrOLD  42867  pw2f1ocnv  42994  aomclem6  43016  hbt  43087  rgspnmin  43128  oasubex  43248  oaabsb  43256  nnoeomeqom  43274  omcl2  43295  naddgeoa  43356  naddwordnexlem4  43363  oaltom  43367  omltoe  43369  minregex  43496  cnvssb  43548  trclubgNEW  43580  dfrcl2  43636  fvmptiunrelexplb0da  43647  relexp0a  43678  cotrcltrcl  43687  trclimalb2  43688  cotrclrcl  43704  isotone2  44011  k0004ss1  44113  fnresdmss  45075  mptelpm  45083  ssnnf1octb  45101  uzfissfz  45241  iuneqfzuzlem  45249  xlimliminflimsup  45783  icccncfext  45808  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  fourierdlem41  46069  fourierdlem70  46097  fourierdlem71  46098  fourierdlem80  46107  fourierdlem113  46140  ioorrnopnlem  46225  ioorrnopnxrlem  46227  salgenss  46257  dfsalgen2  46262  subsaliuncllem  46278  iundjiun  46381  meadjiunlem  46386  meaiunlelem  46389  meaiuninclem  46401  meaiininclem  46407  omeunle  46437  carageniuncllem2  46443  caratheodorylem1  46447  caratheodorylem2  46448  hoissre  46465  ovnsubaddlem1  46491  hoidmvlelem3  46518  ovnhoilem1  46522  ovnhoilem2  46523  ovnhoi  46524  ovncvr2  46532  voncmpl  46542  hspmbllem2  46548  hspmbl  46550  opnvonmbllem1  46553  vonmblss  46561  ovnsubadd2lem  46566  vonioolem2  46602  preimageiingt  46641  preimaleiinlt  46642  issmfd  46656  issmfdf  46658  sssmf  46659  cnfsmf  46661  issmfled  46678  issmfgtd  46682  smfadd  46686  smfrec  46710  smfmul  46716  smfmulc1  46717  smfpimbor1lem2  46720  smfsuplem1  46732  smflimsuplem1  46741  smflimsuplem7  46747  sprssspr  47355  isubgrsubgr  47739  uspgrimprop  47757  uhgrimisgrgriclem  47782  uspgrlimlem3  47814  linc1  48154