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

Theorem sseqtrd 4004
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 3996 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 233 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3933
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 2790
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 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  sseqtrrd  4005  uniintsn  4904  fssdmd  6522  oeeui  8217  nnaword2  8245  oaabs2  8261  erssxp  8301  fipwuni  8878  cantnflem3  9142  ficardun2  9613  ackbij1lem12  9641  ackbij1b  9649  fin1a2lem13  9822  winafp  10107  ioodisj  12856  reltrclfv  14365  prodss  15289  mrcssv  16873  mrcsscl  16879  mrcuni  16880  mressmrcd  16886  mreexexlem2d  16904  mreexexlem3d  16905  mreexfidimd  16909  subcss2  17101  resssetc  17340  funcsetcres2  17341  estrres  17377  poslubdg  17747  ipodrsfi  17761  acsmap2d  17777  mrelatlub  17784  mreclatBAD  17785  subsubm  17969  subsubg  18240  trivsubgd  18243  trivnsgd  18262  oppglsm  18696  subglsm  18728  lsmdisj  18736  gsumval3  18956  dprdres  19079  dprdss  19080  dprd2da  19093  dmdprdsplit2lem  19096  ablfac1b  19121  pgpfac1lem3  19128  issubdrg  19489  subsubrg  19490  islssd  19636  lspun  19688  lspssp  19689  lsslsp  19716  lsmssspx  19789  lspabs2  19821  lspabs3  19822  lspsolvlem  19843  lbsextlem3  19861  mplbas2  20179  gsumply1subr  20330  qsssubdrg  20532  obselocv  20800  lsslindf  20902  tgcl  21505  basgen  21524  tgfiss  21527  bastop1  21529  bastop2  21530  clsss2  21608  elcls3  21619  topssnei  21660  neiptopnei  21668  neitr  21716  restcls  21717  restlp  21719  ordtrest2  21740  iscncl  21805  cncls2  21809  cncls  21810  cnntr  21811  lmcls  21838  tgcmp  21937  cmpcld  21938  uncmp  21939  hauscmplem  21942  cmpfi  21944  clsconn  21966  2ndcsb  21985  2ndcctbss  21991  2ndcomap  21994  nllyrest  22022  1stckgenlem  22089  kgencn2  22093  kgen2cn  22095  ptbasfi  22117  txcld  22139  txcls  22140  txbasval  22142  neitx  22143  ptcld  22149  ptclsg  22151  txnlly  22173  hausdiag  22181  txkgen  22188  xkopt  22191  xkopjcn  22192  xkococnlem  22195  cnmpt1res  22212  cnmpt2res  22213  imasnopn  22226  imasncld  22227  imasncls  22228  qtopcld  22249  qtoprest  22253  qtopcmap  22255  kqcldsat  22269  kqreglem2  22278  kqnrmlem2  22280  hmeontr  22305  neifil  22416  fgtr  22426  trnei  22428  uffixfr  22459  uffix2  22460  uffixsn  22461  elflim  22507  flimclslem  22520  fclsopn  22550  fclscmpi  22565  fclscmp  22566  alexsubALTlem3  22585  alexsubALT  22587  ptcmplem3  22590  subgntr  22642  opnsubg  22643  clssubg  22644  clsnsg  22645  cldsubg  22646  tgpconncompeqg  22647  snclseqg  22651  tsmsgsum  22674  tsmsid  22675  tgptsmscld  22686  ustssco  22750  utop2nei  22786  utop3cls  22787  utopreg  22788  cnextucn  22839  ressprdsds  22908  lpbl  23040  met2ndci  23059  prdsxmslem2  23066  metustexhalf  23093  psmetutop  23104  tgioo  23331  metdstri  23386  metdseq0  23389  xlebnum  23496  clsocv  23780  metelcls  23835  metsscmetcld  23845  cmetss  23846  relcmpcmet  23848  cmpcmet  23849  minveclem4a  23960  uniioovol  24107  uniioombllem3  24113  limcres  24411  dvbss  24426  perfdvf  24428  dvreslem  24434  dvres2lem  24435  dvcnp2  24444  dvaddbr  24462  dvmulbr  24463  dvcmulf  24469  dvcj  24474  dvnfre  24476  dvmptres2  24486  dvmptcmul  24488  dvmptntr  24495  dvlip2  24519  dvcnvrelem2  24542  ftc1cn  24567  dvntaylp  24886  taylthlem1  24888  ulmdvlem3  24917  pserulm  24937  shsub2  29029  spanssoc  29053  shub2  29087  ococin  29112  ssjo  29151  chub2  29212  spanpr  29284  elnlfn  29632  mdslj1i  30023  mdslmd3i  30036  mdexchi  30039  chirredlem1  30094  atcvat3i  30100  mdsymlem1  30107  mdsymlem5  30111  imadifxp  30279  fnpreimac  30344  suppovss  30354  symgcom2  30655  pmtrcnelor  30662  cycpmco2f1  30693  drgextlsp  30895  lvecdim0  30904  lbslsat  30913  dimkerim  30922  fedgmullem2  30925  fedgmul  30926  qtophaus  30999  locfinreflem  31003  fsumcvg4  31092  esum2d  31251  omsmon  31455  omssubadd  31457  carsgclctun  31478  sitgclg  31499  eulerpartlemgf  31536  reprpmtf1o  31796  cvmscld  32417  cvmliftmolem1  32425  cvmlift2lem9  32455  cvmlift2lem11  32457  cvmlift3lem6  32468  nodense  33093  opnregcld  33575  ivthALT  33580  neibastop2  33606  fnemeet1  33611  fnejoin1  33613  pibt2  34580  poimirlem11  34784  poimirlem12  34785  poimirlem30  34803  ftc1cnnc  34847  sstotbnd  34934  ssbnd  34947  heibor1lem  34968  heiborlem3  34972  heibor  34980  lsmsat  36024  lssats  36028  lcvexchlem3  36052  lsatcvat3  36068  lkrscss  36114  lkrpssN  36179  pmod1i  36864  pclbtwnN  36913  pclunN  36914  pclss2polN  36937  pcl0N  36938  sspmaplubN  36941  paddunN  36943  pnonsingN  36949  pclfinclN  36966  osumcllem4N  36975  dia2dimlem13  38092  dvhopellsm  38133  dvadiaN  38144  dicelval1stN  38204  dicelval2nd  38205  dihssxp  38268  dihvalrel  38295  dochsscl  38384  dihoml4  38393  dochnoncon  38407  dvh3dim3N  38465  lcfrlem2  38559  lcfrlem5  38562  lcfr  38601  lcdlsp  38637  mapdsn  38657  mapdlsm  38680  mapdpglem1  38688  mapdindp0  38735  hlhilocv  38973  rntrclfvOAI  39166  ismrcd1  39173  ismrcd2  39174  coeq0i  39228  hbtlem6  39607  rgspnval  39646  iocinico  39696  trclubNEW  39857  ntrk2imkb  40265  isotone1  40276  k0004ss3  40381  iccdifprioo  41668  limsupequzmptlem  41885  cncfuni  42045  cncfiooicclem1  42052  dvresntr  42078  dvmptresicc  42080  itgsubsticclem  42136  fourierdlem42  42311  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  qndenserrn  42461  prsal  42480  intsaluni  42489  sssalgen  42495  dfsalgen2  42501  sge0split  42568  ismeannd  42626  caragensspw  42668  caragendifcl  42673  carageniuncl  42682  caratheodorylem1  42685  hoicvrrex  42715  ovnssle  42720  ovn02  42727  ovnsubadd  42731  hoidmv1le  42753  ovnlecvr2  42769  ovncvr2  42770  isvonmbl  42797  vonmblss  42799  ovolval4lem2  42809  ovnovollem1  42815  ovnovollem2  42816  incsmf  42896  decsmf  42920  uspgropssxp  43896  subsubmgm  43941
  Copyright terms: Public domain W3C validator