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

Theorem sseq1d 3773
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 3767 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  sseq12d  3775  eqsstrd  3780  snssgOLD  4461  ssiun2s  4716  disjxiun  4801  treq  4910  iunopeqop  5131  preddowncl  5868  funimass1  6132  feq1  6187  fvmptss  6454  fvimacnvi  6494  fvimacnvALT  6499  knatar  6770  ovmptss  7426  fnsuppres  7491  imacosupp  7504  wrecseq123  7577  wfrlem1  7583  wfrlem3  7585  wfrdmcl  7592  wfrlem15  7598  wfrlem17  7600  dfrecs3  7638  oaordi  7795  oaword2  7802  oawordeulem  7803  omword1  7822  oewordri  7841  oeordsuc  7843  nnaordi  7867  nnawordex  7886  ereq1  7918  elpm2r  8041  inficl  8496  fipwss  8500  dffi3  8502  hartogslem1  8612  inf3lema  8694  inf3lemd  8697  cantnfle  8741  cantnflem2  8760  trcl  8777  tcmin  8790  rankr1ai  8834  rankxplim  8915  scottex  8921  scott0  8922  scottexs  8923  scott0s  8924  karden  8931  cardne  8981  cardaleph  9102  ackbij2  9257  cflim2  9277  cfslb  9280  coftr  9287  fin23lem15  9348  fin23lem32  9358  fin23lem34  9360  fin23lem35  9361  fin23lem36  9362  fin23lem41  9366  isf32lem1  9367  itunitc1  9434  axdc3lem2  9465  ttukeylem1  9523  fpwwe2cbv  9644  fpwwe2lem2  9646  fpwwe2  9657  fpwwecbv  9658  fpwwelem  9659  canthwelem  9664  canthwe  9665  wunex2  9752  wuncval2  9761  eltsk2g  9765  tskpwss  9766  inar1  9789  grothpw  9840  grothpwex  9841  axgroth6  9842  grothac  9844  peano5uzti  11659  fsuppmapnn0fiub0  12987  relexpnndm  13980  rtrclreclem4  14000  dfrtrcl2  14001  lo1o1  14462  o1lo1  14467  o1lo12  14468  lo1eq  14498  rlimeq  14499  isercoll  14597  prmreclem4  15825  vdwmc  15884  vdwlem1  15887  vdwlem2  15888  vdwlem12  15898  vdwlem13  15899  ramval  15914  ramz2  15930  ramub1lem1  15932  isacs2  16515  isacs1i  16519  mreacs  16520  acsfn  16521  rescabs  16694  ipole  17359  ipodrsima  17366  isacs5  17373  symgsssg  18087  psgnunilem5  18114  sylow1  18218  efgval2  18337  efgsfo  18352  frgpuplem  18385  gsumzf1o  18513  gsumzoppg  18544  dprdcntz  18607  islbs2  19356  frlmssuvc1  20335  frlmssuvc2  20336  frlmsslsp  20337  pptbas  21014  pnfnei  21226  mnfnei  21227  iscnp  21243  iscnp4  21269  cnntr  21281  cnconst2  21289  cnpresti  21294  cnprest  21295  isreg  21338  isnrm  21341  isnrm2  21364  perfcls  21371  isreg2  21383  hauscmplem  21411  1stcfb  21450  1stcelcls  21466  1stccnp  21467  txbas  21572  ptbasfi  21586  xkoopn  21594  xkoccn  21624  txcnp  21625  ptcnplem  21626  txdis  21637  txdis1cn  21640  txtube  21645  txkgen  21657  xkohaus  21658  xkoptsub  21659  xkoco1cn  21662  xkoco2cn  21663  xkococnlem  21664  xkococn  21665  xkoinjcn  21692  kqreglem1  21746  kqreglem2  21747  kqnrmlem1  21748  kqnrmlem2  21749  reghmph  21798  nrmhmph  21799  trfil2  21892  ufileu  21924  elfm  21952  elfm2  21953  elfm3  21955  imaelfm  21956  rnelfm  21958  fmfnfmlem2  21960  fmfnfmlem4  21962  fmco  21966  elflim2  21969  flffbas  22000  lmflf  22010  txflf  22011  fclscf  22030  flimfnfcls  22033  cnextcn  22072  symgtgp  22106  ghmcnp  22119  qustgplem  22125  eltsms  22137  ustval  22207  ust0  22224  trust  22234  utoptop  22239  restutop  22242  restutopopn  22243  utopsnneiplem  22252  ucncn  22290  fmucnd  22297  cfilufg  22298  trcfilu  22299  neipcfilu  22301  blssps  22430  blss  22431  ssblex  22434  blin2  22435  metss2  22518  metrest  22530  metcnp3  22546  metustexhalf  22562  metustbl  22572  psmetutop  22573  xrsmopn  22816  recld2  22818  icccmplem1  22826  icccmplem2  22827  icccmp  22829  reconnlem2  22831  lebnumlem3  22963  lebnum  22964  xlebnum  22965  lebnumii  22966  nmhmcn  23120  cfilfval  23262  caubl  23306  caublcls  23307  bcthlem1  23321  bcth  23326  ovolfiniun  23469  ovoliunlem3  23472  ovoliun  23473  ovoliun2  23474  ovoliunnul  23475  voliunlem3  23520  dyadmax  23566  dyadmbllem  23567  dyadmbl  23568  opnmbllem  23569  ellimc2  23840  limcnlp  23841  ellimc3  23842  limcflf  23844  limciun  23857  cpnord  23897  lhop  23978  xrlimcnp  24894  cvxcl  24910  dchrval  25158  ausgrumgri  26261  ausgrusgri  26262  nbgrval  26428  nbgrel  26432  nbgrelOLD  26433  nbumgrvtx  26441  nbgrnself  26454  uvtxel1  26499  uvtxael1OLD  26501  wlkonl1iedg  26771  crctcshwlkn0lem6  26918  2wlkdlem10  27055  1wlkdlem4  27292  3wlkdlem6  27317  3wlkdlem10  27321  eupth2lem3lem4  27383  frcond1  27420  frgr1v  27425  nfrgr2v  27426  frgr3vlem1  27427  frgr3vlem2  27428  frgr3v  27429  4cycl2vnunb  27444  n4cyclfrgr  27445  isssp  27888  ubthlem1  28035  shmodi  28558  chsupid  28580  chsscon3  28668  spansncvi  28820  mdslmd1lem3  29495  mdslmd1lem4  29496  mdsymlem5  29575  dmdbr5ati  29590  dmdbr6ati  29591  dmdbr7ati  29592  ssiun2sf  29685  fpwrelmapffslem  29816  txomap  30210  locfinreflem  30216  tpr2rico  30267  pnfneige0  30306  rrhre  30374  prodindf  30394  dya2icoseg2  30649  omsfval  30665  eulerpartlemt0  30740  eulerpartgbij  30743  eulerpartlemr  30745  eulerpartlemgs2  30751  eulerpartlemn  30752  eulerpart  30753  bnj517  31262  bnj1014  31337  bnj1015  31338  bnj1123  31361  bnj1125  31367  bnj1450  31425  bnj1452  31427  kur14  31505  cvmliftlem15  31587  cvmlift2lem12  31603  cvmlift2lem13  31604  mclsval  31767  mclsax  31773  mclsppslem  31787  dfpo2  31952  trpredlem1  32032  trpredmintr  32036  frecseq123  32083  frrlem1  32086  frrlem3  32088  frrlem4  32089  frrlem5e  32094  noetalem5  32173  opnrebl  32621  opnrebl2  32622  ivthALT  32636  neibastop2lem  32661  fnemeet1  32667  filnetlem1  32679  filnetlem4  32682  csbwrecsg  33484  lindsenlbs  33717  ptrecube  33722  poimirlem32  33754  opnmbllem0  33758  mblfinlem1  33759  mblfinlem2  33760  mblfinlem3  33761  ovoliunnfl  33764  ex-ovoliunnfl  33765  voliunnfl  33766  totbndbnd  33901  heibor1lem  33921  heiborlem10  33932  scottexf  34289  scott0f  34290  relcnveq2  34418  elrelscnveq2  34566  dfcnvrefrels2  34599  dfcnvrefrel2  34601  symrefref2  34632  lcv1  34831  lfl1dim  34911  lfl1dim2N  34912  paddasslem17  35625  dihglblem6  37131  dochvalr  37148  dochord3  37163  lpolconN  37278  lcfls1lem  37325  mapdffval  37417  mapdfval  37418  mapdsn2  37433  mapd0  37456  lspindp5  37561  mapdh8ab  37568  ismrcd1  37763  nacsfix  37777  setindtr  38093  hbtlem6  38201  clcnvlem  38432  iunrelexpmin1  38502  iunrelexpmin2  38506  relexp0a  38510  cotrcltrcl  38519  trclimalb2  38520  cotrclrcl  38536  sbcheg  38575  clsk1indlem1  38845  isotone1  38848  isotone2  38849  ntrclsiso  38867  ntrclsk2  38868  k0004lem1  38947  k0004lem3  38949  ssdec  39764  iinssd  39813  iinssdf  39827  ssnnf1octb  39881  iooiinicc  40272  iooiinioc  40286  icccncfext  40603  fourierdlem41  40868  meaiininclem  41206  hoidmvlelem3  41317  hoidmvle  41320  opnvonmbllem1  41352  opnvonmbl  41354  iinhoiicclem  41393  smflim  41491  smflimsuplem7  41538  uspgrsprf  42264  dfrngc2  42482  setrecseq  42942  setrec1lem4  42947  setrec2fun  42949
  Copyright terms: Public domain W3C validator