MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstrd Structured version   Visualization version   GIF version

Theorem eqsstrd 3980
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
StepHypRef Expression
1 eqsstrd.2 . 2 (𝜑𝐵𝐶)
2 eqsstrd.1 . . 3 (𝜑𝐴 = 𝐵)
32sseq1d 3973 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 256 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3915  df-ss 3925
This theorem is referenced by:  eqsstrrd  3981  eqsstrdi  3996  fpr2g  7157  tfisi  7787  suppssof1  8122  suppss2  8123  onfununi  8279  oawordeulem  8493  oeeui  8541  nnawordex  8576  oaabslem  8585  oaabs2  8587  omabslem  8588  omabs  8589  pw2f1olem  8978  fodomr  9030  fival  9306  dffi3  9325  ordtypelem7  9418  ordtypelem8  9419  wemapso2lem  9446  cantnflt2  9567  cantnflem1  9583  tcss  9638  tcel  9639  r1val1  9680  rankuni2b  9747  tcrank  9778  cardonle  9851  harval2  9891  ackbij2  10137  cfub  10143  cflecard  10147  cfflb  10153  isf32lem8  10254  itunitc1  10314  ttukeylem7  10409  fpwwe2lem8  10532  wuncss  10639  wuncval2  10641  grur1a  10713  trclfvub  14852  cotrtrclfv  14857  relexpfld  14894  rtrclreclem4  14906  limsupgre  15323  isercolllem3  15511  4sqlem19  16795  vdwlem1  16813  vdwlem12  16824  ramub1lem1  16858  setsstruct2  17006  ressress  17089  imasaddfnlem  17370  imasaddflem  17372  imasvscafn  17379  imasvscaf  17381  imasless  17382  isohom  17619  ressffth  17785  acsfiindd  18402  acsmap2d  18404  dirref  18450  mndind  18598  f1omvdco2  19189  pmtrfrn  19199  symgsssg  19208  symggen  19211  psgnunilem1  19234  sylow2alem2  19359  lsmssv  19384  smndlsmidm  19397  gsumzres  19645  dprdlub  19764  dprdf1  19771  dprdsn  19774  dprdcntz2  19776  dprd2dlem1  19779  dprd2da  19780  dmdprdsplit2lem  19783  ablfac1eu  19811  drnglpir  20676  znleval  20914  evpmss  20943  frlmsplit2  21132  f1lindf  21181  issubassa2  21248  mplsubglem  21357  evlslem4  21436  evlseu  21445  mhpaddcl  21493  mhpinvcl  21494  lpsscls  22444  tgrest  22462  resttopon  22464  rest0  22472  restfpw  22482  ordtrest  22505  ordtrest2  22507  lmcnp  22607  tgcmp  22704  uncmp  22706  hauscmplem  22709  1stcfb  22748  2ndcdisj  22759  dissnref  22831  kgencmp  22848  xkouni  22902  prdstopn  22931  txtube  22943  txcmplem2  22945  xkoptsub  22957  xkopt  22958  xkococnlem  22962  qtoprest  23020  imastopn  23023  kqdisj  23035  reghmph  23096  nrmhmph  23097  fbssfi  23140  trfilss  23192  trfg  23194  elfm3  23253  alexsubALTlem3  23352  alexsubALT  23354  cnextf  23369  cnextcn  23370  clsnsg  23413  tgpconncompeqg  23415  qustgphaus  23426  trust  23533  ustuqtop3  23547  neipcfilu  23600  metequiv2  23818  prdsxmslem2  23837  metustfbas  23865  icccmplem1  24137  metdstri  24166  pi1addf  24362  pi1addval  24363  caubl  24624  caublcls  24625  relcmpcmet  24634  minveclem4  24748  hlhil  24759  ovolficcss  24785  uniioombllem3a  24900  uniioombllem3  24901  dyadss  24910  opnmbllem  24917  i1fima2  24995  limcfval  25188  dvfval  25213  dvnres  25247  dvivth  25326  lhop  25332  taylf  25672  xrlimcnp  26270  jensen  26290  ppisval  26405  chtlepsi  26506  chpub  26520  noextend  26966  nosupbday  27005  noinfbday  27020  scutun12  27101  scutbdaybnd  27106  scutbdaybnd2  27107  scutbdaylt  27109  cofcut1  27188  cofcutr  27192  iscgrglt  27285  chssoc  30267  mdsl0  31081  mdexchi  31106  atcvat3i  31167  dmdbr5ati  31193  funimass4f  31380  xrofsup  31498  swrdrn2  31634  gsumpart  31723  pmtrcnel  31766  tocycfvres1  31785  tocycfvres2  31786  cycpmco2lem6  31806  cycpmconjvlem  31816  cycpmconjslem2  31830  nsgmgc  32016  idlsrgmulrss1  32075  idlsrgmulrss2  32076  fedgmullem1  32144  fedgmullem2  32145  ist0cld  32226  locfinreflem  32233  cmpcref  32243  zarcls0  32261  zarclsiin  32264  zarcmplem  32274  cnvordtrestixx  32306  ordtrestNEW  32314  ordtrest2NEW  32316  pnfneige0  32344  sigagenss  32560  imambfm  32674  dya2iocress  32686  dya2icoseg  32689  dya2iocucvr  32696  ballotlemro  32934  ftc2re  33023  bnj1097  33405  bnj1452  33476  cvmlift3lem6  33730  msubrn  33935  mclsssv  33970  mclsind  33976  cofonr  34230  liness  34668  neibastop2lem  34770  opnmbllem0  36052  mblfinlem2  36054  isbndx  36179  isbnd2  36180  ssbnd  36185  heiborlem3  36210  igenmin  36461  lsatlss  37396  lsmsat  37408  lsatfixedN  37409  lssats  37412  lpssat  37413  lssatle  37415  lssat  37416  lsatcvat3  37452  paddssat  38215  paddasslem17  38237  pmodlem2  38248  hlmod1i  38257  pl42lem4N  38383  diassdvaN  39461  dia2dimlem10  39474  cdlemn4a  39600  cdlemn5pre  39601  dihord5apre  39663  lclkrlem2e  39912  lclkrlem2p  39923  lclkrlem2v  39929  lclkrslem2  39939  lclkrs  39940  lcfrlem25  39968  lcfrlem35  39978  mapdval2N  40031  mapdpglem8  40080  mapdpglem13  40085  baerlem3lem2  40111  mapdindp2  40122  hdmap11lem2  40243  prjspnssbas  40868  elrfi  40926  isnacs3  40942  mzpf  40968  mzpindd  40978  diophrw  40991  eldiophss  41006  rmxyelqirrOLD  41143  pw2f1ocnv  41270  aomclem6  41295  hbt  41366  rgspnmin  41407  oasubex  41530  nnoeomeqom  41554  omcl2  41573  minregex  41717  cnvssb  41769  trclubgNEW  41801  dfrcl2  41857  fvmptiunrelexplb0da  41868  relexp0a  41899  cotrcltrcl  41908  trclimalb2  41909  cotrclrcl  41925  isotone2  42232  k0004ss1  42334  fnresdmss  43290  mptelpm  43298  ssnnf1octb  43319  uzfissfz  43465  iuneqfzuzlem  43473  xlimliminflimsup  44004  icccncfext  44029  dvnprodlem1  44088  dvnprodlem2  44089  dvnprodlem3  44090  fourierdlem41  44290  fourierdlem70  44318  fourierdlem71  44319  fourierdlem80  44328  fourierdlem113  44361  ioorrnopnlem  44446  ioorrnopnxrlem  44448  salgenss  44478  dfsalgen2  44483  subsaliuncllem  44499  iundjiun  44602  meadjiunlem  44607  meaiunlelem  44610  meaiuninclem  44622  meaiininclem  44628  omeunle  44658  carageniuncllem2  44664  caratheodorylem1  44668  caratheodorylem2  44669  hoissre  44686  ovnsubaddlem1  44712  hoidmvlelem3  44739  ovnhoilem1  44743  ovnhoilem2  44744  ovnhoi  44745  ovncvr2  44753  voncmpl  44763  hspmbllem2  44769  hspmbl  44771  opnvonmbllem1  44774  vonmblss  44782  ovnsubadd2lem  44787  vonioolem2  44823  preimageiingt  44862  preimaleiinlt  44863  issmfd  44877  issmfdf  44879  sssmf  44880  cnfsmf  44882  issmfled  44899  issmfgtd  44903  smfadd  44907  smfrec  44931  smfmul  44937  smfmulc1  44938  smfpimbor1lem2  44941  smfsuplem1  44953  smflimsuplem1  44962  smflimsuplem7  44968  sprssspr  45574  linc1  46407
  Copyright terms: Public domain W3C validator