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

Theorem sseq1d 3617
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 3611 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  sseq12d  3619  eqsstrd  3624  snssg  4303  ssiun2s  4537  disjxiun  4619  disjxiunOLD  4620  treq  4728  iunopeqop  4951  preddowncl  5676  funimass1  5939  feq1  5993  fvmptss  6259  fvimacnvi  6297  fvimacnvALT  6302  knatar  6572  ovmptss  7218  fnsuppres  7282  imacosupp  7295  wrecseq123  7368  wfrlem1  7374  wfrlem3  7376  wfrdmcl  7383  wfrlem15  7389  wfrlem17  7391  dfrecs3  7429  oaordi  7586  oaword2  7593  oawordeulem  7594  omword1  7613  oewordri  7632  oeordsuc  7634  nnaordi  7658  nnawordex  7677  ereq1  7709  elpm2r  7835  inficl  8291  fipwss  8295  dffi3  8297  hartogslem1  8407  inf3lema  8481  inf3lemd  8484  cantnfle  8528  cantnflem2  8547  trcl  8564  tcmin  8577  rankr1ai  8621  rankxplim  8702  scottex  8708  scott0  8709  scottexs  8710  scott0s  8711  karden  8718  cardne  8751  cardaleph  8872  ackbij2  9025  cflim2  9045  cfslb  9048  coftr  9055  fin23lem15  9116  fin23lem32  9126  fin23lem34  9128  fin23lem35  9129  fin23lem36  9130  fin23lem41  9134  isf32lem1  9135  itunitc1  9202  axdc3lem2  9233  ttukeylem1  9291  fpwwe2cbv  9412  fpwwe2lem2  9414  fpwwe2  9425  fpwwecbv  9426  fpwwelem  9427  canthwelem  9432  canthwe  9433  wunex2  9520  wuncval2  9529  eltsk2g  9533  tskpwss  9534  inar1  9557  grothpw  9608  grothpwex  9609  axgroth6  9610  grothac  9612  peano5uzti  11427  fsuppmapnn0fiub0  12749  relexpnndm  13731  rtrclreclem4  13751  dfrtrcl2  13752  lo1o1  14213  o1lo1  14218  o1lo12  14219  lo1eq  14249  rlimeq  14250  isercoll  14348  prmreclem4  15566  vdwmc  15625  vdwlem1  15628  vdwlem2  15629  vdwlem12  15639  vdwlem13  15640  ramval  15655  ramz2  15671  ramub1lem1  15673  isacs2  16254  isacs1i  16258  mreacs  16259  acsfn  16260  rescabs  16433  ipole  17098  ipodrsima  17105  isacs5  17112  symgsssg  17827  psgnunilem5  17854  sylow1  17958  efgval2  18077  efgsfo  18092  frgpuplem  18125  gsumzf1o  18253  gsumzoppg  18284  dprdcntz  18347  islbs2  19094  frlmssuvc1  20073  frlmssuvc2  20074  frlmsslsp  20075  pptbas  20752  pnfnei  20964  mnfnei  20965  iscnp  20981  iscnp4  21007  cnntr  21019  cnconst2  21027  cnpresti  21032  cnprest  21033  isreg  21076  isnrm  21079  isnrm2  21102  perfcls  21109  isreg2  21121  hauscmplem  21149  1stcfb  21188  1stcelcls  21204  1stccnp  21205  txbas  21310  ptbasfi  21324  xkoopn  21332  xkoccn  21362  txcnp  21363  ptcnplem  21364  txdis  21375  txdis1cn  21378  txtube  21383  txkgen  21395  xkohaus  21396  xkoptsub  21397  xkoco1cn  21400  xkoco2cn  21401  xkococnlem  21402  xkococn  21403  xkoinjcn  21430  kqreglem1  21484  kqreglem2  21485  kqnrmlem1  21486  kqnrmlem2  21487  reghmph  21536  nrmhmph  21537  trfil2  21631  ufileu  21663  elfm  21691  elfm2  21692  elfm3  21694  imaelfm  21695  rnelfm  21697  fmfnfmlem2  21699  fmfnfmlem4  21701  fmco  21705  elflim2  21708  flffbas  21739  lmflf  21749  txflf  21750  fclscf  21769  flimfnfcls  21772  cnextcn  21811  symgtgp  21845  ghmcnp  21858  qustgplem  21864  eltsms  21876  ustval  21946  ust0  21963  trust  21973  utoptop  21978  restutop  21981  restutopopn  21982  utopsnneiplem  21991  ucncn  22029  fmucnd  22036  cfilufg  22037  trcfilu  22038  neipcfilu  22040  blssps  22169  blss  22170  ssblex  22173  blin2  22174  metss2  22257  metrest  22269  metcnp3  22285  metustexhalf  22301  metustbl  22311  psmetutop  22312  xrsmopn  22555  recld2  22557  icccmplem1  22565  icccmplem2  22566  icccmp  22568  reconnlem2  22570  lebnumlem3  22702  lebnum  22703  xlebnum  22704  lebnumii  22705  nmhmcn  22860  cfilfval  23002  caubl  23046  caublcls  23047  bcthlem1  23061  bcth  23066  ovolfiniun  23209  ovoliunlem3  23212  ovoliun  23213  ovoliun2  23214  ovoliunnul  23215  voliunlem3  23260  dyadmax  23306  dyadmbllem  23307  dyadmbl  23308  opnmbllem  23309  ellimc2  23581  limcnlp  23582  ellimc3  23583  limcflf  23585  limciun  23598  cpnord  23638  lhop  23717  xrlimcnp  24629  cvxcl  24645  dchrval  24893  ausgrumgri  25989  ausgrusgri  25990  nbgrval  26155  nbgrel  26159  nbumgrvtx  26163  nbgrnself  26178  uvtxael1  26217  wlkonl1iedg  26464  crctcshwlkn0lem6  26610  2wlkdlem10  26734  1wlkdlem4  26900  3wlkdlem6  26925  3wlkdlem10  26929  eupth2lem3lem4  26991  frcond1  27030  frgr1v  27033  nfrgr2v  27034  frgr3vlem1  27035  frgr3vlem2  27036  frgr3v  27037  4cycl2vnunb  27052  n4cyclfrgr  27053  isssp  27467  ubthlem1  27614  shmodi  28137  chsupid  28159  chsscon3  28247  spansncvi  28399  mdslmd1lem3  29074  mdslmd1lem4  29075  mdsymlem5  29154  dmdbr5ati  29169  dmdbr6ati  29170  dmdbr7ati  29171  ssiun2sf  29264  fpwrelmapffslem  29391  txomap  29725  locfinreflem  29731  tpr2rico  29782  pnfneige0  29821  rrhre  29889  dya2icoseg2  30163  omsfval  30179  eulerpartlemt0  30254  eulerpartgbij  30257  eulerpartlemr  30259  eulerpartlemgs2  30265  eulerpartlemn  30266  eulerpart  30267  bnj517  30716  bnj1014  30791  bnj1015  30792  bnj1123  30815  bnj1125  30821  bnj1450  30879  bnj1452  30881  kur14  30959  cvmliftlem15  31041  cvmlift2lem12  31057  cvmlift2lem13  31058  mclsval  31221  mclsax  31227  mclsppslem  31241  dfpo2  31406  trpredlem1  31481  trpredmintr  31485  frrlem1  31534  frrlem4  31537  frrlem5e  31542  nobndup  31616  nobnddown  31617  opnrebl  32010  opnrebl2  32011  ivthALT  32025  neibastop2lem  32050  fnemeet1  32056  filnetlem1  32068  filnetlem4  32071  csbwrecsg  32844  lindsenlbs  33075  ptrecube  33080  poimirlem32  33112  opnmbllem0  33116  mblfinlem1  33117  mblfinlem2  33118  mblfinlem3  33119  ovoliunnfl  33122  ex-ovoliunnfl  33123  voliunnfl  33124  totbndbnd  33259  heibor1lem  33279  heiborlem10  33290  scottexf  33647  scott0f  33648  lcv1  33847  lfl1dim  33927  lfl1dim2N  33928  paddasslem17  34641  dihglblem6  36148  dochvalr  36165  dochord3  36180  lpolconN  36295  lcfls1lem  36342  mapdffval  36434  mapdfval  36435  mapdsn2  36450  mapd0  36473  lspindp5  36578  mapdh8ab  36585  ismrcd1  36780  nacsfix  36794  setindtr  37110  hbtlem6  37219  clcnvlem  37450  iunrelexpmin1  37520  iunrelexpmin2  37524  relexp0a  37528  cotrcltrcl  37537  trclimalb2  37538  cotrclrcl  37554  sbcheg  37594  clsk1indlem1  37864  isotone1  37867  isotone2  37868  ntrclsiso  37886  ntrclsk2  37887  k0004lem1  37966  k0004lem3  37968  ssdec  38787  iinssd  38839  iinssdf  38854  ssnnf1octb  38891  iooiinicc  39215  iooiinioc  39229  icccncfext  39435  fourierdlem41  39702  meaiininclem  40037  hoidmvlelem3  40148  hoidmvle  40151  opnvonmbllem1  40183  opnvonmbl  40185  iinhoiicclem  40224  smflim  40322  smflimsuplem7  40369  uspgrsprf  41072  dfrngc2  41290  setrecseq  41755  setrec1lem4  41760  setrec2fun  41762
  Copyright terms: Public domain W3C validator