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

Theorem sseq1d 3995
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 3989 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  sseq12d  3997  eqsstrd  4002  ssiun2s  4963  disjxiun  5054  treq  5169  iunopeqop  5402  preddowncl  6168  funimass1  6429  feq1  6488  fvmptss  6772  fvimacnvi  6814  fvimacnvALT  6819  knatar  7099  ovmptss  7777  fnsuppres  7846  imacosuppOLD  7864  wrecseq123  7937  wfrlem1  7943  wfrlem3  7945  wfrdmcl  7952  wfrlem15  7958  wfrlem17  7960  dfrecs3  7998  oaordi  8161  oaword2  8168  oawordeulem  8169  omword1  8188  oewordri  8207  oeordsuc  8209  nnaordi  8233  nnawordex  8252  ereq1  8285  elpm2r  8413  inficl  8877  fipwss  8881  dffi3  8883  hartogslem1  8994  inf3lema  9075  inf3lemd  9078  cantnfle  9122  cantnflem2  9141  trcl  9158  tcmin  9171  rankr1ai  9215  rankxplim  9296  scottex  9302  scott0  9303  scottexs  9304  scott0s  9305  karden  9312  cardne  9382  cardaleph  9503  ackbij2  9653  cflim2  9673  cfslb  9676  coftr  9683  fin23lem15  9744  fin23lem32  9754  fin23lem34  9756  fin23lem35  9757  fin23lem36  9758  fin23lem41  9762  isf32lem1  9763  itunitc1  9830  axdc3lem2  9861  ttukeylem1  9919  fpwwe2cbv  10040  fpwwe2lem2  10042  fpwwe2  10053  fpwwecbv  10054  fpwwelem  10055  canthwelem  10060  canthwe  10061  wunex2  10148  wuncval2  10157  eltsk2g  10161  tskpwss  10162  inar1  10185  grothpw  10236  grothpwex  10237  axgroth6  10238  grothac  10240  peano5uzti  12060  fsuppmapnn0fiub0  13349  relexpnndm  14388  rtrclreclem4  14408  dfrtrcl2  14409  lo1o1  14877  o1lo1  14882  o1lo12  14883  lo1eq  14913  rlimeq  14914  isercoll  15012  prmreclem4  16243  vdwmc  16302  vdwlem1  16305  vdwlem2  16306  vdwlem12  16316  vdwlem13  16317  ramval  16332  ramz2  16348  ramub1lem1  16350  isacs2  16912  isacs1i  16916  mreacs  16917  acsfn  16918  rescabs  17091  ipole  17756  ipodrsima  17763  isacs5  17770  symgsssg  18524  psgnunilem5  18551  sylow1  18657  efgval2  18779  efgsfo  18794  frgpuplem  18827  gsumzf1o  18961  gsumzoppg  18993  dprdcntz  19059  islbs2  19855  ismhp  20262  frlmssuvc1  20866  frlmssuvc2  20867  frlmsslsp  20868  pptbas  21544  pnfnei  21756  mnfnei  21757  iscnp  21773  iscnp4  21799  cnntr  21811  cnconst2  21819  cnpresti  21824  cnprest  21825  isreg  21868  isnrm  21871  isnrm2  21894  perfcls  21901  isreg2  21913  hauscmplem  21942  1stcfb  21981  1stcelcls  21997  1stccnp  21998  txbas  22103  ptbasfi  22117  xkoopn  22125  xkoccn  22155  txcnp  22156  ptcnplem  22157  txdis  22168  txdis1cn  22171  txtube  22176  txkgen  22188  xkohaus  22189  xkoptsub  22190  xkoco1cn  22193  xkoco2cn  22194  xkococnlem  22195  xkococn  22196  xkoinjcn  22223  kqreglem1  22277  kqreglem2  22278  kqnrmlem1  22279  kqnrmlem2  22280  reghmph  22329  nrmhmph  22330  trfil2  22423  ufileu  22455  elfm  22483  elfm2  22484  elfm3  22486  imaelfm  22487  rnelfm  22489  fmfnfmlem2  22491  fmfnfmlem4  22493  fmco  22497  elflim2  22500  flffbas  22531  lmflf  22541  txflf  22542  fclscf  22561  flimfnfcls  22564  cnextcn  22603  symgtgp  22637  ghmcnp  22650  qustgplem  22656  eltsms  22668  ustval  22738  ust0  22755  trust  22765  utoptop  22770  restutop  22773  restutopopn  22774  utopsnneiplem  22783  ucncn  22821  fmucnd  22828  cfilufg  22829  trcfilu  22830  neipcfilu  22832  blssps  22961  blss  22962  ssblex  22965  blin2  22966  metss2  23049  metrest  23061  metcnp3  23077  metustexhalf  23093  metustbl  23103  psmetutop  23104  xrsmopn  23347  recld2  23349  icccmplem1  23357  icccmplem2  23358  icccmp  23360  reconnlem2  23362  lebnumlem3  23494  lebnum  23495  xlebnum  23496  lebnumii  23497  nmhmcn  23651  cfilfval  23794  caubl  23838  caublcls  23839  bcthlem1  23854  bcth  23859  ovolfiniun  24029  ovoliunlem3  24032  ovoliun  24033  ovoliun2  24034  ovoliunnul  24035  voliunlem3  24080  dyadmax  24126  dyadmbllem  24127  dyadmbl  24128  opnmbllem  24129  ellimc2  24402  limcnlp  24403  ellimc3  24404  limcflf  24406  limciun  24419  cpnord  24459  lhop  24540  xrlimcnp  25473  cvxcl  25489  dchrval  25737  ausgrumgri  26879  ausgrusgri  26880  nbgrval  27045  nbgrel  27049  nbumgrvtx  27055  nbgrnself  27068  uvtxel1  27105  wlkonl1iedg  27374  crctcshwlkn0lem6  27520  2wlkdlem10  27641  1wlkdlem4  27846  3wlkdlem6  27871  3wlkdlem10  27875  eupth2lem3lem4  27937  frcond1  27972  frgr1v  27977  nfrgr2v  27978  frgr3vlem1  27979  frgr3vlem2  27980  frgr3v  27981  4cycl2vnunb  27996  n4cyclfrgr  27997  isssp  28428  ubthlem1  28574  shmodi  29094  chsupid  29116  chsscon3  29204  spansncvi  29356  mdslmd1lem3  30031  mdslmd1lem4  30032  mdsymlem5  30111  dmdbr5ati  30126  dmdbr6ati  30127  dmdbr7ati  30128  ssiun2sf  30239  fpwrelmapffslem  30394  txomap  30997  locfinreflem  31003  tpr2rico  31054  pnfneige0  31093  rrhre  31161  prodindf  31181  dya2icoseg2  31435  omsfval  31451  eulerpartlemt0  31526  eulerpartgbij  31529  eulerpartlemr  31531  eulerpartlemgs2  31537  eulerpartlemn  31538  eulerpart  31539  bnj517  32056  bnj1014  32131  bnj1015  32132  bnj1123  32155  bnj1125  32161  bnj1450  32219  bnj1452  32221  cplgredgex  32264  kur14  32360  cvmliftlem15  32442  cvmlift2lem12  32458  cvmlift2lem13  32459  mclsval  32707  mclsax  32713  mclsppslem  32727  dfpo2  32888  trpredlem1  32963  trpredmintr  32967  frecseq123  33016  frrlem1  33020  frrlem3  33022  frrlem4  33023  frrlem13  33032  noetalem5  33118  opnrebl  33565  opnrebl2  33566  ivthALT  33580  neibastop2lem  33605  fnemeet1  33611  filnetlem1  33623  filnetlem4  33626  bj-imdirval3  34366  csbwrecsg  34490  rdgssun  34541  lindsadd  34766  lindsenlbs  34768  ptrecube  34773  poimirlem32  34805  opnmbllem0  34809  mblfinlem1  34810  mblfinlem2  34811  mblfinlem3  34812  ovoliunnfl  34815  ex-ovoliunnfl  34816  voliunnfl  34817  totbndbnd  34948  heibor1lem  34968  heiborlem10  34979  scottexf  35327  scott0f  35328  relcnveq2  35461  elrelscnveq2  35613  dfcnvrefrels2  35646  dfcnvrefrel2  35648  symrefref2  35679  lcv1  36057  lfl1dim  36137  lfl1dim2N  36138  paddasslem17  36852  dihglblem6  38356  dochvalr  38373  dochord3  38388  lpolconN  38503  lcfls1lem  38550  mapdffval  38642  mapdfval  38643  mapdsn2  38658  mapd0  38681  lspindp5  38786  mapdh8ab  38793  ismrcd1  39173  nacsfix  39187  setindtr  39499  hbtlem6  39607  clcnvlem  39861  iunrelexpmin1  39931  iunrelexpmin2  39935  relexp0a  39939  cotrcltrcl  39948  trclimalb2  39949  cotrclrcl  39965  sbcheg  40003  clsk1indlem1  40273  isotone1  40276  isotone2  40277  ntrclsiso  40295  ntrclsk2  40296  k0004lem1  40375  k0004lem3  40377  scottelrankd  40460  mnuop123d  40475  mnuprdlem1  40485  mnuprdlem2  40486  mnuunid  40490  mnurndlem1  40494  ssdec  41231  iinssd  41273  iinssdf  41284  ssnnf1octb  41332  iooiinicc  41694  iooiinioc  41708  icccncfext  42046  fourierdlem41  42310  meaiininclem  42645  hoidmvlelem3  42756  hoidmvle  42759  opnvonmbllem1  42791  opnvonmbl  42793  iinhoiicclem  42832  smflim  42930  smflimsuplem7  42977  uspgrsprf  43898  setrecseq  44716  setrec1lem4  44721  setrec2fun  44723
  Copyright terms: Public domain W3C validator