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

Theorem eqsstrd 3601
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 3594 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 245 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  eqsstr3d  3602  syl6eqss  3617  fpr2g  6357  tfisi  6927  suppssof1  7192  suppss2  7193  onfununi  7302  oawordeulem  7498  oeeui  7546  nnawordex  7581  oaabslem  7587  oaabs2  7589  omabslem  7590  omabs  7591  pw2f1olem  7926  fodomr  7973  fival  8178  dffi3  8197  ordtypelem7  8289  ordtypelem8  8290  wemapso2lem  8317  cantnflt2  8430  cantnflem1  8446  tcss  8480  tcel  8481  r1val1  8509  rankuni2b  8576  tcrank  8607  cardonle  8643  harval2  8683  carduniima  8779  ackbij2  8925  cfub  8931  cflecard  8935  cfflb  8941  isf32lem8  9042  itunitc1  9102  ttukeylem7  9197  fpwwe2lem9  9316  wuncss  9423  wuncval2  9425  grur1a  9497  trclfvub  13544  cotrtrclfv  13549  relexpfld  13585  rtrclreclem4  13597  limsupgre  14008  isercolllem3  14193  4sqlem19  15453  vdwlem1  15471  vdwlem12  15482  ramub1lem1  15516  setsstruct  15675  ressress  15713  imasaddfnlem  15959  imasaddflem  15961  imasvscafn  15968  imasvscaf  15970  imasless  15971  isohom  16207  ressffth  16369  acsfiindd  16948  acsmap2d  16950  dirref  17006  mrcmndind  17137  f1omvdco2  17639  pmtrfrn  17649  symgsssg  17658  symggen  17661  psgnunilem1  17684  sylow2alem2  17804  lsmssv  17829  lsmidm  17848  gsumzres  18081  dprdlub  18196  dprdf1  18203  dprdsn  18206  dprdcntz2  18208  dprd2dlem1  18211  dprd2da  18212  dmdprdsplit2lem  18215  ablfac1eu  18243  drnglpir  19022  issubassa2  19114  evlslem4  19277  evlseu  19285  znleval  19669  evpmss  19698  frlmsplit2  19878  f1lindf  19927  lpsscls  20702  tgrest  20720  resttopon  20722  rest0  20730  restfpw  20740  ordtrest  20763  ordtrest2  20765  lmcnp  20865  tgcmp  20961  uncmp  20963  hauscmplem  20966  1stcfb  21005  2ndcdisj  21016  dissnref  21088  kgencmp  21105  xkouni  21159  prdstopn  21188  txtube  21200  txcmplem2  21202  xkoptsub  21214  xkopt  21215  xkococnlem  21219  qtoprest  21277  imastopn  21280  kqdisj  21292  reghmph  21353  nrmhmph  21354  fbssfi  21398  trfilss  21450  trfg  21452  elfm3  21511  alexsubALTlem3  21610  alexsubALT  21612  cnextf  21627  cnextcn  21628  clsnsg  21670  tgpconcompeqg  21672  qustgphaus  21683  trust  21790  ustuqtop3  21804  neipcfilu  21857  metequiv2  22072  prdsxmslem2  22091  metustfbas  22119  icccmplem1  22380  metdstri  22409  pi1addf  22602  pi1addval  22603  caubl  22858  caublcls  22859  relcmpcmet  22867  minveclem4  22955  hlhil  22966  ovolficcss  22989  uniioombllem3a  23102  uniioombllem3  23103  dyadss  23112  opnmbllem  23119  i1fima2  23196  limcfval  23386  dvfval  23411  dvnres  23444  dvivth  23521  lhop  23527  taylf  23863  xrlimcnp  24439  jensen  24459  ppisval  24574  chtlepsi  24675  chpub  24689  iscgrglt  25154  edgss  25674  chssoc  27532  mdsl0  28346  mdexchi  28371  atcvat3i  28432  dmdbr5ati  28458  funimass4f  28611  xrofsup  28716  locfinreflem  29028  cmpcref  29038  cnvordtrestixx  29080  ordtrestNEW  29088  ordtrest2NEW  29090  pnfneige0  29118  sigagenss  29332  imambfm  29444  dya2iocress  29456  dya2icoseg  29459  dya2iocucvr  29466  ballotlemro  29704  bnj1097  30096  bnj1452  30167  cvmlift3lem6  30353  msubrn  30473  mclsssv  30508  mclsind  30514  trpredmintr  30768  nobndlem8  30891  liness  31215  neibastop2lem  31318  opnmbllem0  32398  mblfinlem2  32400  isbndx  32534  isbnd2  32535  ssbnd  32540  heiborlem3  32565  igenmin  32816  lsatlss  33084  lsmsat  33096  lsatfixedN  33097  lssats  33100  lpssat  33101  lssatle  33103  lssat  33104  lsatcvat3  33140  paddssat  33901  paddasslem17  33923  pmodlem2  33934  hlmod1i  33943  pl42lem4N  34069  diassdvaN  35150  dia2dimlem10  35163  cdlemn4a  35289  cdlemn5pre  35290  dihord5apre  35352  lclkrlem2e  35601  lclkrlem2p  35612  lclkrlem2v  35618  lclkrslem2  35628  lclkrs  35629  lcfrlem25  35657  lcfrlem35  35667  mapdval2N  35720  mapdpglem8  35769  mapdpglem13  35774  baerlem3lem2  35800  mapdindp2  35811  hdmap11lem2  35935  elrfi  36058  isnacs3  36074  mzpf  36100  mzpindd  36110  diophrw  36123  eldiophss  36139  rmxyelqirr  36276  pw2f1ocnv  36405  aomclem6  36430  hbt  36502  rgspnmin  36543  cnvssb  36694  trclubgNEW  36727  dfrcl2  36768  fvmptiunrelexplb0da  36779  relexp0a  36810  cotrcltrcl  36819  trclimalb2  36820  cotrclrcl  36836  isotone2  37150  k0004ss1  37252  fnresdmss  38125  mptelpm  38135  founiiun0  38155  ssnnf1octb  38160  uzfissfz  38266  iuneqfzuzlem  38274  icccncfext  38556  dvnprodlem1  38619  dvnprodlem2  38620  dvnprodlem3  38621  fourierdlem41  38824  fourierdlem70  38852  fourierdlem71  38853  fourierdlem80  38862  fourierdlem113  38895  rrxbasefi  38962  ioorrnopnlem  38983  ioorrnopnxrlem  38985  salgenss  39013  dfsalgen2  39018  subsaliuncllem  39034  iundjiun  39136  meadjiunlem  39141  meaiunlelem  39144  meaiuninclem  39156  meaiininclem  39159  omeunle  39189  carageniuncllem2  39195  caratheodorylem1  39199  caratheodorylem2  39200  hoissre  39217  ovnsubaddlem1  39243  hoidmvlelem3  39270  ovnhoilem1  39274  ovnhoilem2  39275  ovnhoi  39276  ovncvr2  39284  voncmpl  39294  hspmbllem2  39300  hspmbl  39302  opnvonmbllem1  39305  vonmblss  39313  ovnsubadd2lem  39318  vonioolem2  39355  preimageiingt  39390  preimaleiinlt  39391  issmfd  39404  issmfdf  39407  sssmf  39408  cnfsmf  39410  issmfled  39427  issmfgtd  39430  smfadd  39434  smfrec  39457  smfmul  39463  smfmulc1  39464  smfpimbor1lem2  39467  uhgredgn0  40342  upgredgss  40346  umgredgss  40347  usgredgss  40371  linc1  41989
  Copyright terms: Public domain W3C validator