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

Theorem sseq1d 3980
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
sseq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sseq1d (𝜑 → (𝐴𝐶𝐵𝐶))

Proof of Theorem sseq1d
StepHypRef Expression
1 sseq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 sseq1 3974 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wss 3915
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  sseq12d  3982  eqsstrd  3987  ssiun2s  5013  disjxiun  5107  treq  5235  iunopeqop  5483  dfpo2  6253  preddowncl  6291  funimass1  6588  feq1  6654  focofo  6774  fvmptss  6965  fvimacnvi  7007  fvimacnvALT  7012  knatar  7307  ovmptss  8030  fnsuppres  8127  frecseq123  8218  csbfrecsg  8220  frrlem1  8222  frrlem3  8224  frrlem4  8225  frrlem13  8234  frrdmcl  8244  fprresex  8246  wrecseq123OLD  8251  wfrlem1OLD  8259  wfrlem3OLD  8261  wfrdmclOLD  8268  wfrlem15OLD  8274  wfrlem17OLD  8276  dfrecs3  8323  dfrecs3OLD  8324  oaordi  8498  oaword2  8505  oawordeulem  8506  omword1  8525  oewordri  8544  oeordsuc  8546  nnaordi  8570  nnawordex  8589  naddcllem  8627  naddunif  8644  ereq1  8662  elpm2r  8790  inficl  9368  fipwss  9372  dffi3  9374  hartogslem1  9485  inf3lema  9567  inf3lemd  9570  cantnfle  9614  cantnflem2  9633  ttrclselem1  9668  trcl  9671  tcmin  9684  rankr1ai  9741  rankxplim  9822  scottex  9828  scott0  9829  scottexs  9830  scott0s  9831  karden  9838  cardne  9908  cardaleph  10032  ackbij2  10186  cflim2  10206  cfslb  10209  coftr  10216  fin23lem15  10277  fin23lem32  10287  fin23lem34  10289  fin23lem35  10290  fin23lem36  10291  fin23lem41  10295  isf32lem1  10296  itunitc1  10363  axdc3lem2  10394  ttukeylem1  10452  fpwwe2cbv  10573  fpwwe2lem2  10575  fpwwe2  10586  fpwwecbv  10587  fpwwelem  10588  canthwelem  10593  canthwe  10594  wunex2  10681  wuncval2  10690  eltsk2g  10694  tskpwss  10695  inar1  10718  grothpw  10769  grothpwex  10770  axgroth6  10771  grothac  10773  peano5uzti  12600  fsuppmapnn0fiub0  13905  relexpnndm  14933  rtrclreclem4  14953  dfrtrcl2  14954  lo1o1  15421  o1lo1  15426  o1lo12  15427  lo1eq  15457  rlimeq  15458  isercoll  15559  prmreclem4  16798  vdwmc  16857  vdwlem1  16860  vdwlem2  16861  vdwlem12  16871  vdwlem13  16872  ramval  16887  ramz2  16903  ramub1lem1  16905  isacs2  17540  isacs1i  17544  mreacs  17545  acsfn  17546  rescabs  17725  rescabsOLD  17726  ipole  18430  ipodrsima  18437  isacs5  18444  symgsssg  19256  psgnunilem5  19283  sylow1  19392  efgval2  19513  efgsfo  19528  frgpuplem  19561  gsumzf1o  19696  gsumzoppg  19728  dprdcntz  19794  islbs2  20631  frlmssuvc1  21216  frlmssuvc2  21217  frlmsslsp  21218  ismhp  21547  pptbas  22374  pnfnei  22587  mnfnei  22588  iscnp  22604  iscnp4  22630  cnntr  22642  cnconst2  22650  cnpresti  22655  cnprest  22656  isreg  22699  isnrm  22702  isnrm2  22725  perfcls  22732  isreg2  22744  hauscmplem  22773  1stcfb  22812  1stcelcls  22828  1stccnp  22829  txbas  22934  ptbasfi  22948  xkoopn  22956  xkoccn  22986  txcnp  22987  ptcnplem  22988  txdis  22999  txdis1cn  23002  txtube  23007  txkgen  23019  xkohaus  23020  xkoptsub  23021  xkoco1cn  23024  xkoco2cn  23025  xkococnlem  23026  xkococn  23027  xkoinjcn  23054  kqreglem1  23108  kqreglem2  23109  kqnrmlem1  23110  kqnrmlem2  23111  reghmph  23160  nrmhmph  23161  trfil2  23254  ufileu  23286  elfm  23314  elfm2  23315  elfm3  23317  imaelfm  23318  rnelfm  23320  fmfnfmlem2  23322  fmfnfmlem4  23324  fmco  23328  elflim2  23331  flffbas  23362  lmflf  23372  txflf  23373  fclscf  23392  flimfnfcls  23395  cnextcn  23434  symgtgp  23473  ghmcnp  23482  qustgplem  23488  eltsms  23500  ustval  23570  ust0  23587  trust  23597  utoptop  23602  restutop  23605  restutopopn  23606  utopsnneiplem  23615  ucncn  23653  fmucnd  23660  cfilufg  23661  trcfilu  23662  neipcfilu  23664  blssps  23793  blss  23794  ssblex  23797  blin2  23798  metss2  23884  metrest  23896  metcnp3  23912  metustexhalf  23928  metustbl  23938  psmetutop  23939  xrsmopn  24191  recld2  24193  icccmplem1  24201  icccmplem2  24202  icccmp  24204  reconnlem2  24206  lebnumlem3  24342  lebnum  24343  xlebnum  24344  lebnumii  24345  nmhmcn  24499  cfilfval  24644  caubl  24688  caublcls  24689  bcthlem1  24704  bcth  24709  ovolfiniun  24881  ovoliunlem3  24884  ovoliun  24885  ovoliun2  24886  ovoliunnul  24887  voliunlem3  24932  dyadmax  24978  dyadmbllem  24979  dyadmbl  24980  opnmbllem  24981  ellimc2  25257  limcnlp  25258  ellimc3  25259  limcflf  25261  limciun  25274  cpnord  25315  lhop  25396  xrlimcnp  26334  cvxcl  26350  dchrval  26598  noetalem2  27106  madebdayim  27239  madebdaylemold  27249  madebday  27251  mulsproplem1  27401  ausgrumgri  28160  ausgrusgri  28161  nbgrval  28326  nbgrel  28330  nbumgrvtx  28336  nbgrnself  28349  uvtxel1  28386  wlkonl1iedg  28655  crctcshwlkn0lem6  28802  2wlkdlem10  28922  1wlkdlem4  29126  3wlkdlem6  29151  3wlkdlem10  29155  eupth2lem3lem4  29217  frcond1  29252  frgr1v  29257  nfrgr2v  29258  frgr3vlem1  29259  frgr3vlem2  29260  frgr3v  29261  4cycl2vnunb  29276  n4cyclfrgr  29277  isssp  29708  ubthlem1  29854  shmodi  30374  chsupid  30396  chsscon3  30484  spansncvi  30636  mdslmd1lem3  31311  mdslmd1lem4  31312  mdsymlem5  31391  dmdbr5ati  31406  dmdbr6ati  31407  dmdbr7ati  31408  ssiun2sf  31520  fpwrelmapffslem  31691  pwrssmgc  31902  fldgenval  32121  txomap  32455  locfinreflem  32461  tpr2rico  32533  pnfneige0  32572  rrhre  32642  prodindf  32662  dya2icoseg2  32918  omsfval  32934  eulerpartlemt0  33009  eulerpartgbij  33012  eulerpartlemr  33014  eulerpartlemgs2  33020  eulerpartlemn  33021  eulerpart  33022  bnj517  33537  bnj1014  33613  bnj1015  33614  bnj1123  33638  bnj1125  33644  bnj1450  33702  bnj1452  33704  cplgredgex  33754  kur14  33850  cvmliftlem15  33932  cvmlift2lem12  33948  cvmlift2lem13  33949  mclsval  34197  mclsax  34203  mclsppslem  34217  opnrebl  34821  opnrebl2  34822  ivthALT  34836  neibastop2lem  34861  fnemeet1  34867  filnetlem1  34879  filnetlem4  34882  bj-imdirval3  35684  bj-imdiridlem  35685  rdgssun  35878  lindsadd  36100  lindsenlbs  36102  ptrecube  36107  poimirlem32  36139  opnmbllem0  36143  mblfinlem1  36144  mblfinlem2  36145  mblfinlem3  36146  ovoliunnfl  36149  ex-ovoliunnfl  36150  voliunnfl  36151  totbndbnd  36277  heibor1lem  36297  heiborlem10  36308  scottexf  36656  scott0f  36657  relcnveq2  36813  cnvref4  36840  elrelscnveq2  36984  dfcnvrefrels2  37019  dfcnvrefrel2  37021  symrefref2  37054  lcv1  37532  lfl1dim  37612  lfl1dim2N  37613  paddasslem17  38328  dihglblem6  39832  dochvalr  39849  dochord3  39864  lpolconN  39979  lcfls1lem  40026  mapdffval  40118  mapdfval  40119  mapdsn2  40134  mapd0  40157  lspindp5  40262  mapdh8ab  40269  ismrcd1  41050  nacsfix  41064  setindtr  41377  hbtlem6  41485  oaabsb  41658  naddwordnexlem4  41747  clcnvlem  41969  iunrelexpmin1  42054  iunrelexpmin2  42058  relexp0a  42062  cotrcltrcl  42071  trclimalb2  42072  cotrclrcl  42088  sbcheg  42125  clsk1indlem1  42391  isotone1  42394  isotone2  42395  ntrclsiso  42413  ntrclsk2  42414  k0004lem1  42493  k0004lem3  42495  scottelrankd  42601  mnuop123d  42616  mnuprdlem1  42626  mnuprdlem2  42627  mnuunid  42631  mnurndlem1  42635  ssdec  43372  iinssd  43415  iinssdf  43423  ssnnf1octb  43488  iooiinicc  43854  iooiinioc  43868  icccncfext  44202  fourierdlem41  44463  meaiininclem  44801  hoidmvlelem3  44912  hoidmvle  44915  opnvonmbllem1  44947  opnvonmbl  44949  iinhoiicclem  44988  smflim  45092  smflimsuplem7  45141  uspgrsprf  46122  iscnrm3r  47055  iscnrm3l  47058  setrecseq  47204  setrec1lem4  47209  setrec2fun  47211
  Copyright terms: Public domain W3C validator