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

Theorem sseqtrd 3983
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 3975 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 231 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926
This theorem is referenced by:  sseqtrrd  3984  uniintsn  4947  fssdmd  6683  oeeui  8517  nnaword2  8545  oaabs2  8563  erssxp  8605  fipwuni  9296  cantnflem3  9561  ficardun2  10072  ficardun2OLD  10073  ackbij1lem12  10101  ackbij1b  10109  fin1a2lem13  10282  winafp  10567  ioodisj  13328  reltrclfv  14836  prodss  15765  mrcssv  17429  mrcsscl  17435  mrcuni  17436  mressmrcd  17442  mreexexlem2d  17460  mreexexlem3d  17461  mreexfidimd  17465  subcss2  17664  resssetc  17913  funcsetcres2  17914  estrres  17962  poslubdg  18238  ipodrsfi  18363  acsmap2d  18379  mrelatlub  18386  mreclatBAD  18387  subsubm  18562  subsubg  18884  trivsubgd  18888  trivnsgd  18907  oppglsm  19354  subglsm  19385  lsmdisj  19393  gsumval3  19614  dprdres  19737  dprdss  19738  dprd2da  19751  dmdprdsplit2lem  19754  ablfac1b  19779  pgpfac1lem3  19786  issubdrg  20171  subsubrg  20172  islssd  20320  lspun  20372  lspssp  20373  lsslsp  20400  lsmssspx  20473  lspabs2  20505  lspabs3  20506  lspsolvlem  20527  lbsextlem3  20545  qsssubdrg  20780  obselocv  21058  lsslindf  21160  mplbas2  21366  gsumply1subr  21528  tgcl  22242  basgen  22261  tgfiss  22264  bastop1  22266  bastop2  22267  clsss2  22346  elcls3  22357  topssnei  22398  neiptopnei  22406  neitr  22454  restcls  22455  restlp  22457  ordtrest2  22478  iscncl  22543  cncls2  22547  cncls  22548  cnntr  22549  lmcls  22576  tgcmp  22675  cmpcld  22676  uncmp  22677  hauscmplem  22680  cmpfi  22682  clsconn  22704  2ndcsb  22723  2ndcctbss  22729  2ndcomap  22732  nllyrest  22760  1stckgenlem  22827  kgencn2  22831  kgen2cn  22833  ptbasfi  22855  txcld  22877  txcls  22878  txbasval  22880  neitx  22881  ptcld  22887  ptclsg  22889  txnlly  22911  hausdiag  22919  txkgen  22926  xkopt  22929  xkopjcn  22930  xkococnlem  22933  cnmpt1res  22950  cnmpt2res  22951  imasnopn  22964  imasncld  22965  imasncls  22966  qtopcld  22987  qtoprest  22991  qtopcmap  22993  kqcldsat  23007  kqreglem2  23016  kqnrmlem2  23018  hmeontr  23043  neifil  23154  fgtr  23164  trnei  23166  uffixfr  23197  uffix2  23198  uffixsn  23199  elflim  23245  flimclslem  23258  fclsopn  23288  fclscmpi  23303  fclscmp  23304  alexsubALTlem3  23323  alexsubALT  23325  ptcmplem3  23328  subgntr  23381  opnsubg  23382  clssubg  23383  clsnsg  23384  cldsubg  23385  tgpconncompeqg  23386  snclseqg  23390  tsmsgsum  23413  tsmsid  23414  tgptsmscld  23425  ustssco  23489  utop2nei  23525  utop3cls  23526  utopreg  23527  cnextucn  23578  ressprdsds  23647  lpbl  23782  met2ndci  23801  prdsxmslem2  23808  metustexhalf  23835  psmetutop  23846  tgioo  24082  metdstri  24137  metdseq0  24140  xlebnum  24251  clsocv  24537  metelcls  24592  metsscmetcld  24602  cmetss  24603  relcmpcmet  24605  cmpcmet  24606  minveclem4a  24717  uniioovol  24866  uniioombllem3  24872  limcres  25173  dvbss  25188  perfdvf  25190  dvreslem  25196  dvres2lem  25197  dvmptresicc  25203  dvcnp2  25207  dvaddbr  25225  dvmulbr  25226  dvcmulf  25232  dvcj  25237  dvnfre  25239  dvmptres2  25249  dvmptcmul  25251  dvmptntr  25258  dvlip2  25282  dvcnvrelem2  25305  ftc1cn  25330  dvntaylp  25653  taylthlem1  25655  ulmdvlem3  25684  pserulm  25704  nodense  26963  shsub2  30066  spanssoc  30090  shub2  30124  ococin  30149  ssjo  30188  chub2  30249  spanpr  30321  elnlfn  30669  mdslj1i  31060  mdslmd3i  31073  mdexchi  31076  chirredlem1  31131  atcvat3i  31137  mdsymlem1  31144  mdsymlem5  31148  imadifxp  31317  fnpreimac  31385  suppovss  31394  symgcom2  31730  pmtrcnelor  31737  cycpmco2f1  31768  1fldgenq  31883  0ringidl  31992  elrspunidl  31993  0ringprmidl  32012  idlsrgmulrss1  32043  idlsrgmulrss2  32044  drgextlsp  32079  lvecdim0  32088  lbslsat  32097  dimkerim  32106  fedgmullem2  32109  fedgmul  32110  qtophaus  32191  locfinreflem  32195  rspecbas  32220  zarclssn  32228  zarmxt1  32235  zarcmplem  32236  fsumcvg4  32305  esum2d  32466  omsmon  32672  omssubadd  32674  carsgclctun  32695  sitgclg  32716  eulerpartlemgf  32753  reprpmtf1o  33013  cvmscld  33641  cvmliftmolem1  33649  cvmlift2lem9  33679  cvmlift2lem11  33681  cvmlift3lem6  33692  opnregcld  34698  ivthALT  34703  neibastop2  34729  fnemeet1  34734  fnejoin1  34736  pibt2  35784  poimirlem11  35985  poimirlem12  35986  poimirlem30  36004  ftc1cnnc  36046  sstotbnd  36130  ssbnd  36143  heibor1lem  36164  heiborlem3  36168  heibor  36176  lsmsat  37366  lssats  37370  lcvexchlem3  37394  lsatcvat3  37410  lkrscss  37456  lkrpssN  37521  pmod1i  38207  pclbtwnN  38256  pclunN  38257  pclss2polN  38280  pcl0N  38281  sspmaplubN  38284  paddunN  38286  pnonsingN  38292  pclfinclN  38309  osumcllem4N  38318  dia2dimlem13  39435  dvhopellsm  39476  dvadiaN  39487  dicelval1stN  39547  dicelval2nd  39548  dihssxp  39611  dihvalrel  39638  dochsscl  39727  dihoml4  39736  dochnoncon  39750  dvh3dim3N  39808  lcfrlem2  39902  lcfrlem5  39905  lcfr  39944  lcdlsp  39980  mapdsn  40000  mapdlsm  40023  mapdpglem1  40031  mapdindp0  40078  hlhilocv  40320  rntrclfvOAI  40880  ismrcd1  40887  ismrcd2  40888  coeq0i  40942  hbtlem6  41322  rgspnval  41361  iocinico  41412  omabs2  41423  trclubNEW  41654  ntrk2imkb  42074  isotone1  42085  k0004ss3  42190  iccdifprioo  43509  limsupequzmptlem  43724  cncfuni  43882  cncfiooicclem1  43889  dvresntr  43914  itgsubsticclem  43971  fourierdlem42  44145  fourierdlem48  44150  fourierdlem49  44151  fourierdlem50  44152  qndenserrn  44295  prsal  44314  intsaluni  44325  sssalgen  44331  dfsalgen2  44337  sge0split  44405  ismeannd  44463  caragensspw  44505  caragendifcl  44510  carageniuncl  44519  caratheodorylem1  44522  hoicvrrex  44552  ovnssle  44557  ovn02  44564  ovnsubadd  44568  hoidmv1le  44590  ovnlecvr2  44606  ovncvr2  44607  isvonmbl  44634  vonmblss  44636  ovolval4lem2  44646  ovnovollem1  44652  ovnovollem2  44653  incsmf  44738  decsmf  44763  uspgropssxp  45801  subsubmgm  45846  mreuniss  46687  restcls2lem  46700  restcls2  46701  cnneiima  46704
  Copyright terms: Public domain W3C validator