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

Theorem sseqtrd 4006
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrd.1 (𝜑𝐴𝐵)
sseqtrd.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
sseqtrd (𝜑𝐴𝐶)

Proof of Theorem sseqtrd
StepHypRef Expression
1 sseqtrd.1 . 2 (𝜑𝐴𝐵)
2 sseqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32sseq2d 3998 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 233 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:  sseqtrrd  4007  uniintsn  4906  fssdmd  6523  oeeui  8218  nnaword2  8246  oaabs2  8262  erssxp  8302  fipwuni  8879  cantnflem3  9143  ficardun2  9614  ackbij1lem12  9642  ackbij1b  9650  fin1a2lem13  9823  winafp  10108  ioodisj  12858  reltrclfv  14367  prodss  15291  mrcssv  16875  mrcsscl  16881  mrcuni  16882  mressmrcd  16888  mreexexlem2d  16906  mreexexlem3d  16907  mreexfidimd  16911  subcss2  17103  resssetc  17342  funcsetcres2  17343  estrres  17379  poslubdg  17749  ipodrsfi  17763  acsmap2d  17779  mrelatlub  17786  mreclatBAD  17787  subsubm  17971  subsubg  18242  trivsubgd  18245  trivnsgd  18264  oppglsm  18698  subglsm  18730  lsmdisj  18738  gsumval3  18958  dprdres  19081  dprdss  19082  dprd2da  19095  dmdprdsplit2lem  19098  ablfac1b  19123  pgpfac1lem3  19130  issubdrg  19491  subsubrg  19492  islssd  19638  lspun  19690  lspssp  19691  lsslsp  19718  lsmssspx  19791  lspabs2  19823  lspabs3  19824  lspsolvlem  19845  lbsextlem3  19863  mplbas2  20181  gsumply1subr  20332  qsssubdrg  20534  obselocv  20802  lsslindf  20904  tgcl  21507  basgen  21526  tgfiss  21529  bastop1  21531  bastop2  21532  clsss2  21610  elcls3  21621  topssnei  21662  neiptopnei  21670  neitr  21718  restcls  21719  restlp  21721  ordtrest2  21742  iscncl  21807  cncls2  21811  cncls  21812  cnntr  21813  lmcls  21840  tgcmp  21939  cmpcld  21940  uncmp  21941  hauscmplem  21944  cmpfi  21946  clsconn  21968  2ndcsb  21987  2ndcctbss  21993  2ndcomap  21996  nllyrest  22024  1stckgenlem  22091  kgencn2  22095  kgen2cn  22097  ptbasfi  22119  txcld  22141  txcls  22142  txbasval  22144  neitx  22145  ptcld  22151  ptclsg  22153  txnlly  22175  hausdiag  22183  txkgen  22190  xkopt  22193  xkopjcn  22194  xkococnlem  22197  cnmpt1res  22214  cnmpt2res  22215  imasnopn  22228  imasncld  22229  imasncls  22230  qtopcld  22251  qtoprest  22255  qtopcmap  22257  kqcldsat  22271  kqreglem2  22280  kqnrmlem2  22282  hmeontr  22307  neifil  22418  fgtr  22428  trnei  22430  uffixfr  22461  uffix2  22462  uffixsn  22463  elflim  22509  flimclslem  22522  fclsopn  22552  fclscmpi  22567  fclscmp  22568  alexsubALTlem3  22587  alexsubALT  22589  ptcmplem3  22592  subgntr  22644  opnsubg  22645  clssubg  22646  clsnsg  22647  cldsubg  22648  tgpconncompeqg  22649  snclseqg  22653  tsmsgsum  22676  tsmsid  22677  tgptsmscld  22688  ustssco  22752  utop2nei  22788  utop3cls  22789  utopreg  22790  cnextucn  22841  ressprdsds  22910  lpbl  23042  met2ndci  23061  prdsxmslem2  23068  metustexhalf  23095  psmetutop  23106  tgioo  23333  metdstri  23388  metdseq0  23391  xlebnum  23498  clsocv  23782  metelcls  23837  metsscmetcld  23847  cmetss  23848  relcmpcmet  23850  cmpcmet  23851  minveclem4a  23962  uniioovol  24109  uniioombllem3  24115  limcres  24413  dvbss  24428  perfdvf  24430  dvreslem  24436  dvres2lem  24437  dvcnp2  24446  dvaddbr  24464  dvmulbr  24465  dvcmulf  24471  dvcj  24476  dvnfre  24478  dvmptres2  24488  dvmptcmul  24490  dvmptntr  24497  dvlip2  24521  dvcnvrelem2  24544  ftc1cn  24569  dvntaylp  24888  taylthlem1  24890  ulmdvlem3  24919  pserulm  24939  shsub2  29030  spanssoc  29054  shub2  29088  ococin  29113  ssjo  29152  chub2  29213  spanpr  29285  elnlfn  29633  mdslj1i  30024  mdslmd3i  30037  mdexchi  30040  chirredlem1  30095  atcvat3i  30101  mdsymlem1  30108  mdsymlem5  30112  imadifxp  30280  fnpreimac  30345  suppovss  30355  symgcom2  30656  pmtrcnelor  30663  cycpmco2f1  30694  drgextlsp  30896  lvecdim0  30905  lbslsat  30914  dimkerim  30923  fedgmullem2  30926  fedgmul  30927  qtophaus  31000  locfinreflem  31004  fsumcvg4  31093  esum2d  31252  omsmon  31456  omssubadd  31458  carsgclctun  31479  sitgclg  31500  eulerpartlemgf  31537  reprpmtf1o  31797  cvmscld  32418  cvmliftmolem1  32426  cvmlift2lem9  32456  cvmlift2lem11  32458  cvmlift3lem6  32469  nodense  33094  opnregcld  33576  ivthALT  33581  neibastop2  33607  fnemeet1  33612  fnejoin1  33614  pibt2  34581  poimirlem11  34785  poimirlem12  34786  poimirlem30  34804  ftc1cnnc  34848  sstotbnd  34936  ssbnd  34949  heibor1lem  34970  heiborlem3  34974  heibor  34982  lsmsat  36026  lssats  36030  lcvexchlem3  36054  lsatcvat3  36070  lkrscss  36116  lkrpssN  36181  pmod1i  36866  pclbtwnN  36915  pclunN  36916  pclss2polN  36939  pcl0N  36940  sspmaplubN  36943  paddunN  36945  pnonsingN  36951  pclfinclN  36968  osumcllem4N  36977  dia2dimlem13  38094  dvhopellsm  38135  dvadiaN  38146  dicelval1stN  38206  dicelval2nd  38207  dihssxp  38270  dihvalrel  38297  dochsscl  38386  dihoml4  38395  dochnoncon  38409  dvh3dim3N  38467  lcfrlem2  38561  lcfrlem5  38564  lcfr  38603  lcdlsp  38639  mapdsn  38659  mapdlsm  38682  mapdpglem1  38690  mapdindp0  38737  hlhilocv  38975  rntrclfvOAI  39168  ismrcd1  39175  ismrcd2  39176  coeq0i  39230  hbtlem6  39609  rgspnval  39648  iocinico  39698  trclubNEW  39859  ntrk2imkb  40267  isotone1  40278  k0004ss3  40383  iccdifprioo  41672  limsupequzmptlem  41889  cncfuni  42049  cncfiooicclem1  42056  dvresntr  42082  dvmptresicc  42084  itgsubsticclem  42140  fourierdlem42  42315  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  qndenserrn  42465  prsal  42484  intsaluni  42493  sssalgen  42499  dfsalgen2  42505  sge0split  42572  ismeannd  42630  caragensspw  42672  caragendifcl  42677  carageniuncl  42686  caratheodorylem1  42689  hoicvrrex  42719  ovnssle  42724  ovn02  42731  ovnsubadd  42735  hoidmv1le  42757  ovnlecvr2  42773  ovncvr2  42774  isvonmbl  42801  vonmblss  42803  ovolval4lem2  42813  ovnovollem1  42819  ovnovollem2  42820  incsmf  42900  decsmf  42924  uspgropssxp  43866  subsubmgm  43911
  Copyright terms: Public domain W3C validator