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

Theorem eqsstrd 3956
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 3949 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 260 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wss 3884
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  eqsstrrd  3957  eqsstrdi  3972  fpr2g  6955  tfisi  7557  suppssof1  7850  suppss2  7851  onfununi  7965  oawordeulem  8167  oeeui  8215  nnawordex  8250  oaabslem  8257  oaabs2  8259  omabslem  8260  omabs  8261  pw2f1olem  8608  fodomr  8656  fival  8864  dffi3  8883  ordtypelem7  8976  ordtypelem8  8977  wemapso2lem  9004  cantnflt2  9124  cantnflem1  9140  tcss  9174  tcel  9175  r1val1  9203  rankuni2b  9270  tcrank  9301  cardonle  9374  harval2  9414  ackbij2  9658  cfub  9664  cflecard  9668  cfflb  9674  isf32lem8  9775  itunitc1  9835  ttukeylem7  9930  fpwwe2lem9  10053  wuncss  10160  wuncval2  10162  grur1a  10234  trclfvub  14362  cotrtrclfv  14367  relexpfld  14403  rtrclreclem4  14415  limsupgre  14833  isercolllem3  15018  4sqlem19  16292  vdwlem1  16310  vdwlem12  16321  ramub1lem1  16355  setsstruct2  16516  ressress  16557  imasaddfnlem  16796  imasaddflem  16798  imasvscafn  16805  imasvscaf  16807  imasless  16808  isohom  17041  ressffth  17203  acsfiindd  17782  acsmap2d  17784  dirref  17840  mndind  17987  f1omvdco2  18571  pmtrfrn  18581  symgsssg  18590  symggen  18593  psgnunilem1  18616  sylow2alem2  18738  lsmssv  18763  smndlsmidm  18776  lsmidmOLD  18784  gsumzres  19025  dprdlub  19144  dprdf1  19151  dprdsn  19154  dprdcntz2  19156  dprd2dlem1  19159  dprd2da  19160  dmdprdsplit2lem  19163  ablfac1eu  19191  drnglpir  20022  znleval  20249  evpmss  20278  frlmsplit2  20465  f1lindf  20514  issubassa2  20581  mplsubglem  20675  evlslem4  20750  evlseu  20758  mhpaddcl  20802  mhpinvcl  20803  lpsscls  21749  tgrest  21767  resttopon  21769  rest0  21777  restfpw  21787  ordtrest  21810  ordtrest2  21812  lmcnp  21912  tgcmp  22009  uncmp  22011  hauscmplem  22014  1stcfb  22053  2ndcdisj  22064  dissnref  22136  kgencmp  22153  xkouni  22207  prdstopn  22236  txtube  22248  txcmplem2  22250  xkoptsub  22262  xkopt  22263  xkococnlem  22267  qtoprest  22325  imastopn  22328  kqdisj  22340  reghmph  22401  nrmhmph  22402  fbssfi  22445  trfilss  22497  trfg  22499  elfm3  22558  alexsubALTlem3  22657  alexsubALT  22659  cnextf  22674  cnextcn  22675  clsnsg  22718  tgpconncompeqg  22720  qustgphaus  22731  trust  22838  ustuqtop3  22852  neipcfilu  22905  metequiv2  23120  prdsxmslem2  23139  metustfbas  23167  icccmplem1  23430  metdstri  23459  pi1addf  23655  pi1addval  23656  caubl  23915  caublcls  23916  relcmpcmet  23925  minveclem4  24039  hlhil  24050  ovolficcss  24076  uniioombllem3a  24191  uniioombllem3  24192  dyadss  24201  opnmbllem  24208  i1fima2  24286  limcfval  24478  dvfval  24503  dvnres  24537  dvivth  24616  lhop  24622  taylf  24959  xrlimcnp  25557  jensen  25577  ppisval  25692  chtlepsi  25793  chpub  25807  iscgrglt  26311  chssoc  29282  mdsl0  30096  mdexchi  30121  atcvat3i  30182  dmdbr5ati  30208  funimass4f  30399  xrofsup  30521  swrdrn2  30657  gsumpart  30743  pmtrcnel  30786  tocycfvres1  30805  tocycfvres2  30806  cycpmco2lem6  30826  cycpmconjvlem  30836  cycpmconjslem2  30850  idlsrgmulrss1  31064  idlsrgmulrss2  31065  fedgmullem1  31113  fedgmullem2  31114  ist0cld  31186  locfinreflem  31193  cmpcref  31203  zarcls0  31221  zarclsiin  31224  zarcmplem  31234  cnvordtrestixx  31264  ordtrestNEW  31272  ordtrest2NEW  31274  pnfneige0  31302  sigagenss  31516  imambfm  31628  dya2iocress  31640  dya2icoseg  31643  dya2iocucvr  31650  ballotlemro  31888  ftc2re  31977  bnj1097  32361  bnj1452  32432  cvmlift3lem6  32679  msubrn  32884  mclsssv  32919  mclsind  32925  trpredmintr  33178  noextend  33281  nosupbday  33313  scutun12  33379  scutbdaybnd  33383  scutbdaylt  33384  liness  33714  neibastop2lem  33816  opnmbllem0  35086  mblfinlem2  35088  isbndx  35213  isbnd2  35214  ssbnd  35219  heiborlem3  35244  igenmin  35495  lsatlss  36285  lsmsat  36297  lsatfixedN  36298  lssats  36301  lpssat  36302  lssatle  36304  lssat  36305  lsatcvat3  36341  paddssat  37103  paddasslem17  37125  pmodlem2  37136  hlmod1i  37145  pl42lem4N  37271  diassdvaN  38349  dia2dimlem10  38362  cdlemn4a  38488  cdlemn5pre  38489  dihord5apre  38551  lclkrlem2e  38800  lclkrlem2p  38811  lclkrlem2v  38817  lclkrslem2  38827  lclkrs  38828  lcfrlem25  38856  lcfrlem35  38866  mapdval2N  38919  mapdpglem8  38968  mapdpglem13  38973  baerlem3lem2  38999  mapdindp2  39010  hdmap11lem2  39131  elrfi  39622  isnacs3  39638  mzpf  39664  mzpindd  39674  diophrw  39687  eldiophss  39702  rmxyelqirr  39838  pw2f1ocnv  39965  aomclem6  39990  hbt  40061  rgspnmin  40102  cnvssb  40273  trclubgNEW  40305  dfrcl2  40362  fvmptiunrelexplb0da  40373  relexp0a  40404  cotrcltrcl  40413  trclimalb2  40414  cotrclrcl  40430  isotone2  40739  k0004ss1  40841  fnresdmss  41779  mptelpm  41787  ssnnf1octb  41809  uzfissfz  41945  iuneqfzuzlem  41953  xlimliminflimsup  42491  icccncfext  42516  dvnprodlem1  42575  dvnprodlem2  42576  dvnprodlem3  42577  fourierdlem41  42777  fourierdlem70  42805  fourierdlem71  42806  fourierdlem80  42815  fourierdlem113  42848  ioorrnopnlem  42933  ioorrnopnxrlem  42935  salgenss  42963  dfsalgen2  42968  subsaliuncllem  42984  iundjiun  43086  meadjiunlem  43091  meaiunlelem  43094  meaiuninclem  43106  meaiininclem  43112  omeunle  43142  carageniuncllem2  43148  caratheodorylem1  43152  caratheodorylem2  43153  hoissre  43170  ovnsubaddlem1  43196  hoidmvlelem3  43223  ovnhoilem1  43227  ovnhoilem2  43228  ovnhoi  43229  ovncvr2  43237  voncmpl  43247  hspmbllem2  43253  hspmbl  43255  opnvonmbllem1  43258  vonmblss  43266  ovnsubadd2lem  43271  vonioolem2  43307  preimageiingt  43342  preimaleiinlt  43343  issmfd  43356  issmfdf  43358  sssmf  43359  cnfsmf  43361  issmfled  43378  issmfgtd  43381  smfadd  43385  smfrec  43408  smfmul  43414  smfmulc1  43415  smfpimbor1lem2  43418  smfsuplem1  43429  smflimsuplem1  43438  smflimsuplem7  43444  sprssspr  43985  linc1  44821
  Copyright terms: Public domain W3C validator