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

Theorem sseqtrd 4010
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 4002 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 233 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-in 3946  df-ss 3955
This theorem is referenced by:  sseqtrrd  4011  uniintsn  4910  fssdmd  6525  oeeui  8221  nnaword2  8249  oaabs2  8265  erssxp  8305  fipwuni  8882  cantnflem3  9146  ficardun2  9617  ackbij1lem12  9645  ackbij1b  9653  fin1a2lem13  9826  winafp  10111  ioodisj  12861  reltrclfv  14370  prodss  15294  mrcssv  16878  mrcsscl  16884  mrcuni  16885  mressmrcd  16891  mreexexlem2d  16909  mreexexlem3d  16910  mreexfidimd  16914  subcss2  17106  resssetc  17345  funcsetcres2  17346  estrres  17382  poslubdg  17752  ipodrsfi  17766  acsmap2d  17782  mrelatlub  17789  mreclatBAD  17790  subsubm  17969  subsubg  18235  trivsubgd  18238  trivnsgd  18257  oppglsm  18690  subglsm  18722  lsmdisj  18730  gsumval3  18950  dprdres  19073  dprdss  19074  dprd2da  19087  dmdprdsplit2lem  19090  ablfac1b  19115  pgpfac1lem3  19122  issubdrg  19483  subsubrg  19484  islssd  19630  lspun  19682  lspssp  19683  lsslsp  19710  lsmssspx  19783  lspabs2  19815  lspabs3  19816  lspsolvlem  19837  lbsextlem3  19855  mplbas2  20172  gsumply1subr  20322  qsssubdrg  20523  obselocv  20791  lsslindf  20893  tgcl  21496  basgen  21515  tgfiss  21518  bastop1  21520  bastop2  21521  clsss2  21599  elcls3  21610  topssnei  21651  neiptopnei  21659  neitr  21707  restcls  21708  restlp  21710  ordtrest2  21731  iscncl  21796  cncls2  21800  cncls  21801  cnntr  21802  lmcls  21829  tgcmp  21928  cmpcld  21929  uncmp  21930  hauscmplem  21933  cmpfi  21935  clsconn  21957  2ndcsb  21976  2ndcctbss  21982  2ndcomap  21985  nllyrest  22013  1stckgenlem  22080  kgencn2  22084  kgen2cn  22086  ptbasfi  22108  txcld  22130  txcls  22131  txbasval  22133  neitx  22134  ptcld  22140  ptclsg  22142  txnlly  22164  hausdiag  22172  txkgen  22179  xkopt  22182  xkopjcn  22183  xkococnlem  22186  cnmpt1res  22203  cnmpt2res  22204  imasnopn  22217  imasncld  22218  imasncls  22219  qtopcld  22240  qtoprest  22244  qtopcmap  22246  kqcldsat  22260  kqreglem2  22269  kqnrmlem2  22271  hmeontr  22296  neifil  22407  fgtr  22417  trnei  22419  uffixfr  22450  uffix2  22451  uffixsn  22452  elflim  22498  flimclslem  22511  fclsopn  22541  fclscmpi  22556  fclscmp  22557  alexsubALTlem3  22576  alexsubALT  22578  ptcmplem3  22581  subgntr  22633  opnsubg  22634  clssubg  22635  clsnsg  22636  cldsubg  22637  tgpconncompeqg  22638  snclseqg  22642  tsmsgsum  22665  tsmsid  22666  tgptsmscld  22677  ustssco  22741  utop2nei  22777  utop3cls  22778  utopreg  22779  cnextucn  22830  ressprdsds  22899  lpbl  23031  met2ndci  23050  prdsxmslem2  23057  metustexhalf  23084  psmetutop  23095  tgioo  23322  metdstri  23377  metdseq0  23380  xlebnum  23487  clsocv  23771  metelcls  23826  metsscmetcld  23836  cmetss  23837  relcmpcmet  23839  cmpcmet  23840  minveclem4a  23951  uniioovol  24098  uniioombllem3  24104  limcres  24402  dvbss  24417  perfdvf  24419  dvreslem  24425  dvres2lem  24426  dvcnp2  24435  dvaddbr  24453  dvmulbr  24454  dvcmulf  24460  dvcj  24465  dvnfre  24467  dvmptres2  24477  dvmptcmul  24479  dvmptntr  24486  dvlip2  24510  dvcnvrelem2  24533  ftc1cn  24558  dvntaylp  24877  taylthlem1  24879  ulmdvlem3  24908  pserulm  24928  shsub2  29019  spanssoc  29043  shub2  29077  ococin  29102  ssjo  29141  chub2  29202  spanpr  29274  elnlfn  29622  mdslj1i  30013  mdslmd3i  30026  mdexchi  30029  chirredlem1  30084  atcvat3i  30090  mdsymlem1  30097  mdsymlem5  30101  imadifxp  30269  fnpreimac  30334  suppovss  30344  symgcom2  30645  pmtrcnelor  30652  cycpmco2f1  30683  drgextlsp  30885  lvecdim0  30894  lbslsat  30903  dimkerim  30912  fedgmullem2  30915  fedgmul  30916  qtophaus  30989  locfinreflem  30993  fsumcvg4  31082  esum2d  31241  omsmon  31445  omssubadd  31447  carsgclctun  31468  sitgclg  31489  eulerpartlemgf  31526  reprpmtf1o  31786  cvmscld  32407  cvmliftmolem1  32415  cvmlift2lem9  32445  cvmlift2lem11  32447  cvmlift3lem6  32458  nodense  33083  opnregcld  33565  ivthALT  33570  neibastop2  33596  fnemeet1  33601  fnejoin1  33603  pibt2  34570  poimirlem11  34773  poimirlem12  34774  poimirlem30  34792  ftc1cnnc  34836  sstotbnd  34924  ssbnd  34937  heibor1lem  34958  heiborlem3  34962  heibor  34970  lsmsat  36014  lssats  36018  lcvexchlem3  36042  lsatcvat3  36058  lkrscss  36104  lkrpssN  36169  pmod1i  36854  pclbtwnN  36903  pclunN  36904  pclss2polN  36927  pcl0N  36928  sspmaplubN  36931  paddunN  36933  pnonsingN  36939  pclfinclN  36956  osumcllem4N  36965  dia2dimlem13  38082  dvhopellsm  38123  dvadiaN  38134  dicelval1stN  38194  dicelval2nd  38195  dihssxp  38258  dihvalrel  38285  dochsscl  38374  dihoml4  38383  dochnoncon  38397  dvh3dim3N  38455  lcfrlem2  38549  lcfrlem5  38552  lcfr  38591  lcdlsp  38627  mapdsn  38647  mapdlsm  38670  mapdpglem1  38678  mapdindp0  38725  hlhilocv  38963  rntrclfvOAI  39156  ismrcd1  39163  ismrcd2  39164  coeq0i  39218  hbtlem6  39597  rgspnval  39636  iocinico  39686  trclubNEW  39847  ntrk2imkb  40255  isotone1  40266  k0004ss3  40371  iccdifprioo  41660  limsupequzmptlem  41877  cncfuni  42037  cncfiooicclem1  42044  dvresntr  42070  dvmptresicc  42072  itgsubsticclem  42128  fourierdlem42  42303  fourierdlem48  42308  fourierdlem49  42309  fourierdlem50  42310  qndenserrn  42453  prsal  42472  intsaluni  42481  sssalgen  42487  dfsalgen2  42493  sge0split  42560  ismeannd  42618  caragensspw  42660  caragendifcl  42665  carageniuncl  42674  caratheodorylem1  42677  hoicvrrex  42707  ovnssle  42712  ovn02  42719  ovnsubadd  42723  hoidmv1le  42745  ovnlecvr2  42761  ovncvr2  42762  isvonmbl  42789  vonmblss  42791  ovolval4lem2  42801  ovnovollem1  42807  ovnovollem2  42808  incsmf  42888  decsmf  42912  uspgropssxp  43854  subsubmgm  43899
  Copyright terms: Public domain W3C validator