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

Theorem eqsstrd 4004
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 3997 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 258 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  eqsstrrd  4005  eqsstrdi  4020  fpr2g  6966  tfisi  7561  suppssof1  7854  suppss2  7855  onfununi  7969  oawordeulem  8170  oeeui  8218  nnawordex  8253  oaabslem  8260  oaabs2  8262  omabslem  8263  omabs  8264  pw2f1olem  8610  fodomr  8657  fival  8865  dffi3  8884  ordtypelem7  8977  ordtypelem8  8978  wemapso2lem  9005  cantnflt2  9125  cantnflem1  9141  tcss  9175  tcel  9176  r1val1  9204  rankuni2b  9271  tcrank  9302  cardonle  9375  harval2  9415  ackbij2  9654  cfub  9660  cflecard  9664  cfflb  9670  isf32lem8  9771  itunitc1  9831  ttukeylem7  9926  fpwwe2lem9  10049  wuncss  10156  wuncval2  10158  grur1a  10230  trclfvub  14357  cotrtrclfv  14362  relexpfld  14398  rtrclreclem4  14410  limsupgre  14828  isercolllem3  15013  4sqlem19  16289  vdwlem1  16307  vdwlem12  16318  ramub1lem1  16352  setsstruct2  16511  ressress  16552  imasaddfnlem  16791  imasaddflem  16793  imasvscafn  16800  imasvscaf  16802  imasless  16803  isohom  17036  ressffth  17198  acsfiindd  17777  acsmap2d  17779  dirref  17835  mndind  17982  f1omvdco2  18507  pmtrfrn  18517  symgsssg  18526  symggen  18529  psgnunilem1  18552  sylow2alem2  18674  lsmssv  18699  smndlsmidm  18712  lsmidmOLD  18720  gsumzres  18960  dprdlub  19079  dprdf1  19086  dprdsn  19089  dprdcntz2  19091  dprd2dlem1  19094  dprd2da  19095  dmdprdsplit2lem  19098  ablfac1eu  19126  drnglpir  19956  issubassa2  20051  evlslem4  20218  evlseu  20226  mhpaddcl  20268  mhpinvcl  20269  znleval  20631  evpmss  20660  frlmsplit2  20847  f1lindf  20896  lpsscls  21679  tgrest  21697  resttopon  21699  rest0  21707  restfpw  21717  ordtrest  21740  ordtrest2  21742  lmcnp  21842  tgcmp  21939  uncmp  21941  hauscmplem  21944  1stcfb  21983  2ndcdisj  21994  dissnref  22066  kgencmp  22083  xkouni  22137  prdstopn  22166  txtube  22178  txcmplem2  22180  xkoptsub  22192  xkopt  22193  xkococnlem  22197  qtoprest  22255  imastopn  22258  kqdisj  22270  reghmph  22331  nrmhmph  22332  fbssfi  22375  trfilss  22427  trfg  22429  elfm3  22488  alexsubALTlem3  22587  alexsubALT  22589  cnextf  22604  cnextcn  22605  clsnsg  22647  tgpconncompeqg  22649  qustgphaus  22660  trust  22767  ustuqtop3  22781  neipcfilu  22834  metequiv2  23049  prdsxmslem2  23068  metustfbas  23096  icccmplem1  23359  metdstri  23388  pi1addf  23580  pi1addval  23581  caubl  23840  caublcls  23841  relcmpcmet  23850  minveclem4  23964  hlhil  23975  ovolficcss  23999  uniioombllem3a  24114  uniioombllem3  24115  dyadss  24124  opnmbllem  24131  i1fima2  24209  limcfval  24399  dvfval  24424  dvnres  24457  dvivth  24536  lhop  24542  taylf  24878  xrlimcnp  25474  jensen  25494  ppisval  25609  chtlepsi  25710  chpub  25724  iscgrglt  26228  chssoc  29201  mdsl0  30015  mdexchi  30040  atcvat3i  30101  dmdbr5ati  30127  funimass4f  30311  xrofsup  30419  swrdrn2  30556  pmtrcnel  30661  tocycfvres1  30680  tocycfvres2  30681  cycpmco2lem6  30701  cycpmconjvlem  30711  cycpmconjslem2  30725  fedgmullem1  30925  fedgmullem2  30926  locfinreflem  31004  cmpcref  31014  cnvordtrestixx  31056  ordtrestNEW  31064  ordtrest2NEW  31066  pnfneige0  31094  sigagenss  31308  imambfm  31420  dya2iocress  31432  dya2icoseg  31435  dya2iocucvr  31442  ballotlemro  31680  ftc2re  31769  bnj1097  32151  bnj1452  32222  cvmlift3lem6  32469  msubrn  32674  mclsssv  32709  mclsind  32715  trpredmintr  32968  noextend  33071  nosupbday  33103  scutun12  33169  scutbdaybnd  33173  scutbdaylt  33174  liness  33504  neibastop2lem  33606  opnmbllem0  34810  mblfinlem2  34812  isbndx  34943  isbnd2  34944  ssbnd  34949  heiborlem3  34974  igenmin  35225  lsatlss  36014  lsmsat  36026  lsatfixedN  36027  lssats  36030  lpssat  36031  lssatle  36033  lssat  36034  lsatcvat3  36070  paddssat  36832  paddasslem17  36854  pmodlem2  36865  hlmod1i  36874  pl42lem4N  37000  diassdvaN  38078  dia2dimlem10  38091  cdlemn4a  38217  cdlemn5pre  38218  dihord5apre  38280  lclkrlem2e  38529  lclkrlem2p  38540  lclkrlem2v  38546  lclkrslem2  38556  lclkrs  38557  lcfrlem25  38585  lcfrlem35  38595  mapdval2N  38648  mapdpglem8  38697  mapdpglem13  38702  baerlem3lem2  38728  mapdindp2  38739  hdmap11lem2  38860  elrfi  39171  isnacs3  39187  mzpf  39213  mzpindd  39223  diophrw  39236  eldiophss  39251  rmxyelqirr  39387  pw2f1ocnv  39514  aomclem6  39539  hbt  39610  rgspnmin  39651  cnvssb  39826  trclubgNEW  39858  dfrcl2  39899  fvmptiunrelexplb0da  39910  relexp0a  39941  cotrcltrcl  39950  trclimalb2  39951  cotrclrcl  39967  isotone2  40279  k0004ss1  40381  fnresdmss  41304  mptelpm  41312  ssnnf1octb  41336  uzfissfz  41474  iuneqfzuzlem  41482  xlimliminflimsup  42023  icccncfext  42050  dvnprodlem1  42111  dvnprodlem2  42112  dvnprodlem3  42113  fourierdlem41  42314  fourierdlem70  42342  fourierdlem71  42343  fourierdlem80  42352  fourierdlem113  42385  ioorrnopnlem  42470  ioorrnopnxrlem  42472  salgenss  42500  dfsalgen2  42505  subsaliuncllem  42521  iundjiun  42623  meadjiunlem  42628  meaiunlelem  42631  meaiuninclem  42643  meaiininclem  42649  omeunle  42679  carageniuncllem2  42685  caratheodorylem1  42689  caratheodorylem2  42690  hoissre  42707  ovnsubaddlem1  42733  hoidmvlelem3  42760  ovnhoilem1  42764  ovnhoilem2  42765  ovnhoi  42766  ovncvr2  42774  voncmpl  42784  hspmbllem2  42790  hspmbl  42792  opnvonmbllem1  42795  vonmblss  42803  ovnsubadd2lem  42808  vonioolem2  42844  preimageiingt  42879  preimaleiinlt  42880  issmfd  42893  issmfdf  42895  sssmf  42896  cnfsmf  42898  issmfled  42915  issmfgtd  42918  smfadd  42922  smfrec  42945  smfmul  42951  smfmulc1  42952  smfpimbor1lem2  42955  smfsuplem1  42966  smflimsuplem1  42975  smflimsuplem7  42981  sprssspr  43490  linc1  44378
  Copyright terms: Public domain W3C validator