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

Theorem eqsstrd 3672
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 3665 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 247 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  eqsstr3d  3673  syl6eqss  3688  fpr2g  6516  tfisi  7100  suppssof1  7373  suppss2  7374  onfununi  7483  oawordeulem  7679  oeeui  7727  nnawordex  7762  oaabslem  7768  oaabs2  7770  omabslem  7771  omabs  7772  pw2f1olem  8105  fodomr  8152  fival  8359  dffi3  8378  ordtypelem7  8470  ordtypelem8  8471  wemapso2lem  8498  cantnflt2  8608  cantnflem1  8624  tcss  8658  tcel  8659  r1val1  8687  rankuni2b  8754  tcrank  8785  cardonle  8821  harval2  8861  carduniima  8957  ackbij2  9103  cfub  9109  cflecard  9113  cfflb  9119  isf32lem8  9220  itunitc1  9280  ttukeylem7  9375  fpwwe2lem9  9498  wuncss  9605  wuncval2  9607  grur1a  9679  trclfvub  13792  cotrtrclfv  13797  relexpfld  13833  rtrclreclem4  13845  limsupgre  14256  isercolllem3  14441  4sqlem19  15714  vdwlem1  15732  vdwlem12  15743  ramub1lem1  15777  setsstruct2  15943  setsstructOLD  15946  ressress  15985  imasaddfnlem  16235  imasaddflem  16237  imasvscafn  16244  imasvscaf  16246  imasless  16247  isohom  16483  ressffth  16645  acsfiindd  17224  acsmap2d  17226  dirref  17282  mrcmndind  17413  f1omvdco2  17914  pmtrfrn  17924  symgsssg  17933  symggen  17936  psgnunilem1  17959  sylow2alem2  18079  lsmssv  18104  lsmidm  18123  gsumzres  18356  dprdlub  18471  dprdf1  18478  dprdsn  18481  dprdcntz2  18483  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  ablfac1eu  18518  drnglpir  19301  issubassa2  19393  evlslem4  19556  evlseu  19564  znleval  19951  evpmss  19980  frlmsplit2  20160  f1lindf  20209  lpsscls  20993  tgrest  21011  resttopon  21013  rest0  21021  restfpw  21031  ordtrest  21054  ordtrest2  21056  lmcnp  21156  tgcmp  21252  uncmp  21254  hauscmplem  21257  1stcfb  21296  2ndcdisj  21307  dissnref  21379  kgencmp  21396  xkouni  21450  prdstopn  21479  txtube  21491  txcmplem2  21493  xkoptsub  21505  xkopt  21506  xkococnlem  21510  qtoprest  21568  imastopn  21571  kqdisj  21583  reghmph  21644  nrmhmph  21645  fbssfi  21688  trfilss  21740  trfg  21742  elfm3  21801  alexsubALTlem3  21900  alexsubALT  21902  cnextf  21917  cnextcn  21918  clsnsg  21960  tgpconncompeqg  21962  qustgphaus  21973  trust  22080  ustuqtop3  22094  neipcfilu  22147  metequiv2  22362  prdsxmslem2  22381  metustfbas  22409  icccmplem1  22672  metdstri  22701  pi1addf  22893  pi1addval  22894  caubl  23152  caublcls  23153  relcmpcmet  23161  minveclem4  23249  hlhil  23260  ovolficcss  23284  uniioombllem3a  23398  uniioombllem3  23399  dyadss  23408  opnmbllem  23415  i1fima2  23491  limcfval  23681  dvfval  23706  dvnres  23739  dvivth  23818  lhop  23824  taylf  24160  xrlimcnp  24740  jensen  24760  ppisval  24875  chtlepsi  24976  chpub  24990  iscgrglt  25454  chssoc  28483  mdsl0  29297  mdexchi  29322  atcvat3i  29383  dmdbr5ati  29409  funimass4f  29565  xrofsup  29661  locfinreflem  30035  cmpcref  30045  cnvordtrestixx  30087  ordtrestNEW  30095  ordtrest2NEW  30097  pnfneige0  30125  sigagenss  30340  imambfm  30452  dya2iocress  30464  dya2icoseg  30467  dya2iocucvr  30474  ballotlemro  30712  ftc2re  30804  bnj1097  31175  bnj1452  31246  cvmlift3lem6  31432  msubrn  31552  mclsssv  31587  mclsind  31593  trpredmintr  31855  noextend  31944  nosupbday  31976  scutun12  32042  scutbdaybnd  32046  scutbdaylt  32047  liness  32377  neibastop2lem  32480  opnmbllem0  33575  mblfinlem2  33577  isbndx  33711  isbnd2  33712  ssbnd  33717  heiborlem3  33742  igenmin  33993  lsatlss  34601  lsmsat  34613  lsatfixedN  34614  lssats  34617  lpssat  34618  lssatle  34620  lssat  34621  lsatcvat3  34657  paddssat  35418  paddasslem17  35440  pmodlem2  35451  hlmod1i  35460  pl42lem4N  35586  diassdvaN  36666  dia2dimlem10  36679  cdlemn4a  36805  cdlemn5pre  36806  dihord5apre  36868  lclkrlem2e  37117  lclkrlem2p  37128  lclkrlem2v  37134  lclkrslem2  37144  lclkrs  37145  lcfrlem25  37173  lcfrlem35  37183  mapdval2N  37236  mapdpglem8  37285  mapdpglem13  37290  baerlem3lem2  37316  mapdindp2  37327  hdmap11lem2  37451  elrfi  37574  isnacs3  37590  mzpf  37616  mzpindd  37626  diophrw  37639  eldiophss  37655  rmxyelqirr  37792  pw2f1ocnv  37921  aomclem6  37946  hbt  38017  rgspnmin  38058  cnvssb  38209  trclubgNEW  38242  dfrcl2  38283  fvmptiunrelexplb0da  38294  relexp0a  38325  cotrcltrcl  38334  trclimalb2  38335  cotrclrcl  38351  isotone2  38664  k0004ss1  38766  fnresdmss  39662  mptelpm  39671  founiiun0  39691  ssnnf1octb  39696  uzfissfz  39855  iuneqfzuzlem  39863  icccncfext  40418  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  fourierdlem41  40683  fourierdlem70  40711  fourierdlem71  40712  fourierdlem80  40721  fourierdlem113  40754  rrxbasefi  40821  ioorrnopnlem  40842  ioorrnopnxrlem  40844  salgenss  40872  dfsalgen2  40877  subsaliuncllem  40893  iundjiun  40995  meadjiunlem  41000  meaiunlelem  41003  meaiuninclem  41015  meaiininclem  41021  omeunle  41051  carageniuncllem2  41057  caratheodorylem1  41061  caratheodorylem2  41062  hoissre  41079  ovnsubaddlem1  41105  hoidmvlelem3  41132  ovnhoilem1  41136  ovnhoilem2  41137  ovnhoi  41138  ovncvr2  41146  voncmpl  41156  hspmbllem2  41162  hspmbl  41164  opnvonmbllem1  41167  vonmblss  41175  ovnsubadd2lem  41180  vonioolem2  41216  preimageiingt  41251  preimaleiinlt  41252  issmfd  41265  issmfdf  41267  sssmf  41268  cnfsmf  41270  issmfled  41287  issmfgtd  41290  smfadd  41294  smfrec  41317  smfmul  41323  smfmulc1  41324  smfpimbor1lem2  41327  smfsuplem1  41338  smflimsuplem1  41347  smflimsuplem7  41353  sprssspr  42056  linc1  42539
  Copyright terms: Public domain W3C validator