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

Theorem sseqtrd 3803
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 3795 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 223 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wss 3734
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3741  df-ss 3748
This theorem is referenced by:  sseqtr4d  3804  uniintsn  4672  fssdmd  6240  oeeui  7891  nnaword2  7919  oaabs2  7934  erssxp  7974  fipwuni  8543  cantnflem3  8807  cdainf  9271  ficardun2  9282  ackbij1lem12  9310  ackbij1b  9318  fin1a2lem13  9491  winafp  9776  ioodisj  12516  reltrclfv  14059  prodss  14976  mrcssv  16556  mrcsscl  16562  mrcuni  16563  mressmrcd  16569  mreexexlem2d  16587  mreexexlem3d  16588  mreexfidimd  16592  subcss2  16784  resssetc  17023  funcsetcres2  17024  estrresOLD  17060  estrres  17061  poslubdg  17431  ipodrsfi  17445  acsmap2d  17461  mrelatlub  17468  mreclatBAD  17469  subsubm  17639  subsubg  17897  oppglsm  18337  subglsm  18366  lsmdisj  18374  gsumval3  18590  dprdres  18710  dprdss  18711  dprd2da  18724  dmdprdsplit2lem  18727  ablfac1b  18752  pgpfac1lem3  18759  issubdrg  19090  subsubrg  19091  islssd  19221  lspun  19275  lspssp  19276  lsslsp  19303  lsmssspx  19376  lspabs2  19408  lspabs3  19409  lspsolvlem  19431  lbsextlem3  19450  mplbas2  19760  gsumply1subr  19893  qsssubdrg  20094  obselocv  20364  lsslindf  20461  tgcl  21069  basgen  21088  tgfiss  21091  bastop1  21093  bastop2  21094  clsss2  21172  elcls3  21183  topssnei  21224  neiptopnei  21232  neitr  21280  restcls  21281  restlp  21283  ordtrest2  21304  iscncl  21369  cncls2  21373  cncls  21374  cnntr  21375  lmcls  21402  tgcmp  21500  cmpcld  21501  uncmp  21502  hauscmplem  21505  cmpfi  21507  clsconn  21529  2ndcsb  21548  2ndcctbss  21554  2ndcomap  21557  nllyrest  21585  1stckgenlem  21652  kgencn2  21656  kgen2cn  21658  ptbasfi  21680  txcld  21702  txcls  21703  txbasval  21705  neitx  21706  ptcld  21712  ptclsg  21714  txnlly  21736  hausdiag  21744  txkgen  21751  xkopt  21754  xkopjcn  21755  xkococnlem  21758  cnmpt1res  21775  cnmpt2res  21776  imasnopn  21789  imasncld  21790  imasncls  21791  qtopcld  21812  qtoprest  21816  qtopcmap  21818  kqcldsat  21832  kqreglem2  21841  kqnrmlem2  21843  hmeontr  21868  neifil  21979  fgtr  21989  trnei  21991  uffixfr  22022  uffix2  22023  uffixsn  22024  elflim  22070  flimclslem  22083  fclsopn  22113  fclscmpi  22128  fclscmp  22129  alexsubALTlem3  22148  alexsubALT  22150  ptcmplem3  22153  subgntr  22205  opnsubg  22206  clssubg  22207  clsnsg  22208  cldsubg  22209  tgpconncompeqg  22210  snclseqg  22214  tsmsgsum  22237  tsmsid  22238  tgptsmscld  22249  ustssco  22313  utop2nei  22349  utop3cls  22350  utopreg  22351  cnextucn  22402  ressprdsds  22471  lpbl  22603  met2ndci  22622  prdsxmslem2  22629  metustexhalf  22656  psmetutop  22667  tgioo  22894  metdstri  22949  metdseq0  22952  xlebnum  23059  clsocv  23343  metelcls  23398  metsscmetcld  23408  cmetss  23409  relcmpcmet  23411  cmpcmet  23412  minveclem4a  23506  uniioovol  23653  uniioombllem3  23659  limcres  23957  dvbss  23972  perfdvf  23974  dvreslem  23980  dvres2lem  23981  dvcnp2  23990  dvaddbr  24008  dvmulbr  24009  dvcmulf  24015  dvcj  24020  dvnfre  24022  dvmptres2  24032  dvmptcmul  24034  dvmptntr  24041  dvlip2  24065  dvcnvrelem2  24088  ftc1cn  24113  dvntaylp  24432  taylthlem1  24434  ulmdvlem3  24463  pserulm  24483  shsub2  28663  spanssoc  28687  shub2  28721  ococin  28746  ssjo  28785  chub2  28846  spanpr  28918  elnlfn  29266  mdslj1i  29657  mdslmd3i  29670  mdexchi  29673  chirredlem1  29728  atcvat3i  29734  mdsymlem1  29741  mdsymlem5  29745  imadifxp  29885  qtophaus  30373  locfinreflem  30377  fsumcvg4  30466  esum2d  30625  omsmon  30830  omssubadd  30832  carsgclctun  30853  sitgclg  30874  eulerpartlemgf  30911  reprpmtf1o  31178  cvmscld  31726  cvmliftmolem1  31734  cvmlift2lem9  31764  cvmlift2lem11  31766  cvmlift3lem6  31777  nodense  32309  opnregcld  32791  ivthALT  32796  neibastop2  32822  fnemeet1  32827  fnejoin1  32829  poimirlem11  33867  poimirlem12  33868  poimirlem30  33886  ftc1cnnc  33930  sstotbnd  34019  ssbnd  34032  heibor1lem  34053  heiborlem3  34057  heibor  34065  lsmsat  34987  lssats  34991  lcvexchlem3  35015  lsatcvat3  35031  lkrscss  35077  lkrpssN  35142  pmod1i  35827  pclbtwnN  35876  pclunN  35877  pclss2polN  35900  pcl0N  35901  sspmaplubN  35904  paddunN  35906  pnonsingN  35912  pclfinclN  35929  osumcllem4N  35938  dia2dimlem13  37055  dvhopellsm  37096  dvadiaN  37107  dicelval1stN  37167  dicelval2nd  37168  dihssxp  37231  dihvalrel  37258  dochsscl  37347  dihoml4  37356  dochnoncon  37370  dvh3dim3N  37428  lcfrlem2  37522  lcfrlem5  37525  lcfr  37564  lcdlsp  37600  mapdsn  37620  mapdlsm  37643  mapdpglem1  37651  mapdindp0  37698  hlhilocv  37936  rntrclfvOAI  37958  ismrcd1  37965  ismrcd2  37966  coeq0i  38020  hbtlem6  38402  rgspnval  38441  iocinico  38499  trclubNEW  38627  ntrk2imkb  39035  isotone1  39046  k0004ss3  39151  wessf1ornlem  40044  iccdifprioo  40407  limsupequzmptlem  40624  cncfuni  40763  cncfiooicclem1  40770  dvresntr  40796  dvmptresicc  40798  itgsubsticclem  40854  fourierdlem42  41029  fourierdlem48  41034  fourierdlem49  41035  fourierdlem50  41036  qndenserrn  41182  prsal  41201  intsaluni  41210  sssalgen  41216  dfsalgen2  41222  sge0split  41289  ismeannd  41347  caragensspw  41389  caragendifcl  41394  carageniuncl  41403  caratheodorylem1  41406  hoicvrrex  41436  ovnssle  41441  ovn02  41448  ovnsubadd  41452  hoidmv1le  41474  ovnlecvr2  41490  ovncvr2  41491  isvonmbl  41518  vonmblss  41520  ovolval4lem2  41530  ovnovollem1  41536  ovnovollem2  41537  incsmf  41617  decsmf  41641  uspgropssxp  42447  subsubmgm  42492
  Copyright terms: Public domain W3C validator