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

Theorem sseq1d 3594
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 3588 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  sseq12d  3596  eqsstrd  3601  snssg  4267  ssiun2s  4494  disjxiun  4573  disjxiunOLD  4574  treq  4680  preddowncl  5609  funimass1  5870  feq1  5924  fvmptss  6185  fvimacnvi  6223  fvimacnvALT  6228  knatar  6484  ovmptss  7122  fnsuppres  7186  imacosupp  7199  wrecseq123  7272  wfrlem1  7278  wfrlem3  7280  wfrdmcl  7287  wfrlem15  7293  wfrlem17  7295  dfrecs3  7333  oaordi  7490  oaword2  7497  oawordeulem  7498  omword1  7517  oewordri  7536  oeordsuc  7538  nnaordi  7562  nnawordex  7581  ereq1  7613  elpm2r  7738  inficl  8191  fipwss  8195  dffi3  8197  hartogslem1  8307  inf3lema  8381  inf3lemd  8384  cantnfle  8428  cantnflem2  8447  trcl  8464  tcmin  8477  rankr1ai  8521  rankxplim  8602  scottex  8608  scott0  8609  scottexs  8610  scott0s  8611  karden  8618  cardne  8651  cardaleph  8772  ackbij2  8925  cflim2  8945  cfslb  8948  coftr  8955  fin23lem15  9016  fin23lem32  9026  fin23lem34  9028  fin23lem35  9029  fin23lem36  9030  fin23lem41  9034  isf32lem1  9035  itunitc1  9102  axdc3lem2  9133  ttukeylem1  9191  fpwwe2cbv  9308  fpwwe2lem2  9310  fpwwe2  9321  fpwwecbv  9322  fpwwelem  9323  canthwelem  9328  canthwe  9329  wunex2  9416  wuncval2  9425  eltsk2g  9429  tskpwss  9430  inar1  9453  grothpw  9504  grothpwex  9505  axgroth6  9506  grothac  9508  peano5uzti  11301  fsuppmapnn0fiub0  12612  relexpnndm  13577  rtrclreclem4  13597  dfrtrcl2  13598  lo1o1  14059  o1lo1  14064  o1lo12  14065  lo1eq  14095  rlimeq  14096  isercoll  14194  prmreclem4  15409  vdwmc  15468  vdwlem1  15471  vdwlem2  15472  vdwlem12  15482  vdwlem13  15483  ramval  15498  ramz2  15514  ramub1lem1  15516  isacs2  16085  isacs1i  16089  mreacs  16090  acsfn  16091  rescabs  16264  ipole  16929  ipodrsima  16936  isacs5  16943  symgsssg  17658  psgnunilem5  17685  sylow1  17789  efgval2  17908  efgsfo  17923  frgpuplem  17956  gsumzf1o  18084  gsumzoppg  18115  dprdcntz  18178  islbs2  18923  frlmssuvc1  19899  frlmssuvc2  19900  frlmsslsp  19901  pptbas  20569  pnfnei  20781  mnfnei  20782  iscnp  20798  iscnp4  20824  cnntr  20836  cnconst2  20844  cnpresti  20849  cnprest  20850  isreg  20893  isnrm  20896  isnrm2  20919  perfcls  20926  isreg2  20938  hauscmplem  20966  1stcfb  21005  1stcelcls  21021  1stccnp  21022  txbas  21127  ptbasfi  21141  xkoopn  21149  xkoccn  21179  txcnp  21180  ptcnplem  21181  txdis  21192  txdis1cn  21195  txtube  21200  txkgen  21212  xkohaus  21213  xkoptsub  21214  xkoco1cn  21217  xkoco2cn  21218  xkococnlem  21219  xkococn  21220  xkoinjcn  21247  kqreglem1  21301  kqreglem2  21302  kqnrmlem1  21303  kqnrmlem2  21304  reghmph  21353  nrmhmph  21354  trfil2  21448  ufileu  21480  elfm  21508  elfm2  21509  elfm3  21511  imaelfm  21512  rnelfm  21514  fmfnfmlem2  21516  fmfnfmlem4  21518  fmco  21522  elflim2  21525  flffbas  21556  lmflf  21566  txflf  21567  fclscf  21586  flimfnfcls  21589  cnextcn  21628  symgtgp  21662  ghmcnp  21675  qustgplem  21681  eltsms  21693  ustval  21763  ust0  21780  trust  21790  utoptop  21795  restutop  21798  restutopopn  21799  utopsnneiplem  21808  ucncn  21846  fmucnd  21853  cfilufg  21854  trcfilu  21855  neipcfilu  21857  blssps  21986  blss  21987  ssblex  21990  blin2  21991  metss2  22074  metrest  22086  metcnp3  22102  metustexhalf  22118  metustbl  22128  psmetutop  22129  xrsmopn  22370  recld2  22372  icccmplem1  22380  icccmplem2  22381  icccmp  22383  reconnlem2  22385  lebnumlem3  22517  lebnum  22518  xlebnum  22519  lebnumii  22520  nmhmcn  22675  cfilfval  22814  caubl  22858  caublcls  22859  bcthlem1  22873  bcth  22878  ovolfiniun  23020  ovoliunlem3  23023  ovoliun  23024  ovoliun2  23025  ovoliunnul  23026  voliunlem3  23071  dyadmax  23116  dyadmbllem  23117  dyadmbl  23118  opnmbllem  23119  ellimc2  23391  limcnlp  23392  ellimc3  23393  limcflf  23395  limciun  23408  cpnord  23448  lhop  23527  xrlimcnp  24439  cvxcl  24455  dchrval  24703  frgraunss  26315  frgra1v  26318  frgra2v  26319  frgra3vlem1  26320  frgra3vlem2  26321  frgra3v  26322  4cycl2vnunb  26337  n4cyclfrgra  26338  isssp  26756  ubthlem1  26903  shmodi  27426  chsupid  27448  chsscon3  27536  spansncvi  27688  mdslmd1lem3  28363  mdslmd1lem4  28364  mdsymlem5  28443  dmdbr5ati  28458  dmdbr6ati  28459  dmdbr7ati  28460  ssiun2sf  28553  fpwrelmapffslem  28688  txomap  29022  locfinreflem  29028  tpr2rico  29079  pnfneige0  29118  rrhre  29186  dya2icoseg2  29460  omsfval  29476  eulerpartlemt0  29551  eulerpartgbij  29554  eulerpartlemr  29556  eulerpartlemgs2  29562  eulerpartlemn  29563  eulerpart  29564  bnj517  30002  bnj1014  30077  bnj1015  30078  bnj1123  30101  bnj1125  30107  bnj1450  30165  bnj1452  30167  kur14  30245  cvmliftlem15  30327  cvmlift2lem12  30343  cvmlift2lem13  30344  mclsval  30507  mclsax  30513  mclsppslem  30527  dfpo2  30691  trpredlem1  30764  trpredmintr  30768  frrlem1  30817  frrlem4  30820  frrlem5e  30825  nobndup  30892  nobnddown  30893  nofulllem5  30898  opnrebl  31278  opnrebl2  31279  ivthALT  31293  neibastop2lem  31318  fnemeet1  31324  filnetlem1  31336  filnetlem4  31339  csbwrecsg  32132  lindsenlbs  32357  ptrecube  32362  poimirlem32  32394  opnmbllem0  32398  mblfinlem1  32399  mblfinlem2  32400  mblfinlem3  32401  ovoliunnfl  32404  ex-ovoliunnfl  32405  voliunnfl  32406  totbndbnd  32541  heibor1lem  32561  heiborlem10  32572  scottexf  32929  scott0f  32930  lcv1  33129  lfl1dim  33209  lfl1dim2N  33210  paddasslem17  33923  dihglblem6  35430  dochvalr  35447  dochord3  35462  lpolconN  35577  lcfls1lem  35624  mapdffval  35716  mapdfval  35717  mapdsn2  35732  mapd0  35755  lspindp5  35860  mapdh8ab  35867  ismrcd1  36062  nacsfix  36076  setindtr  36392  hbtlem6  36501  clcnvlem  36732  iunrelexpmin1  36802  iunrelexpmin2  36806  relexp0a  36810  cotrcltrcl  36819  trclimalb2  36820  cotrclrcl  36836  sbcheg  36876  clsk1indlem1  37146  isotone1  37149  isotone2  37150  ntrclsiso  37168  ntrclsk2  37169  k0004lem1  37248  k0004lem3  37250  ssdec  38076  ssnnf1octb  38160  iooiinicc  38399  iooiinioc  38413  icccncfext  38556  fourierdlem41  38824  meaiininclem  39159  hoidmvlelem3  39270  hoidmvle  39273  opnvonmbllem1  39305  opnvonmbl  39307  iinhoiicclem  39347  smflim  39446  iunopeqop  40110  ausgrumgri  40378  ausgrusgri  40379  nbgrval  40541  nbgrel  40545  nbumgrvtx  40549  nbgrnself  40564  uvtxael1  40603  wlkOnl1iedg  40854  crctcsh1wlkn0lem6  40999  21wlkdlem10  41123  11wlkdlem4  41288  31wlkdlem6  41313  31wlkdlem10  41317  eupth2lem3lem4  41380  frcond1  41419  frgr1v  41422  nfrgr2v  41423  frgr3vlem1  41424  frgr3vlem2  41425  frgr3v  41426  4cycl2vnunb-av  41441  n4cyclfrgr  41442  dfrngc2  41745
  Copyright terms: Public domain W3C validator