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

Theorem sseq1d 3665
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 3659 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  sseq12d  3667  eqsstrd  3672  snssgOLD  4349  ssiun2s  4596  disjxiun  4681  disjxiunOLD  4682  treq  4791  iunopeqop  5010  preddowncl  5745  funimass1  6009  feq1  6064  fvmptss  6331  fvimacnvi  6371  fvimacnvALT  6376  knatar  6647  ovmptss  7303  fnsuppres  7367  imacosupp  7380  wrecseq123  7453  wfrlem1  7459  wfrlem3  7461  wfrdmcl  7468  wfrlem15  7474  wfrlem17  7476  dfrecs3  7514  oaordi  7671  oaword2  7678  oawordeulem  7679  omword1  7698  oewordri  7717  oeordsuc  7719  nnaordi  7743  nnawordex  7762  ereq1  7794  elpm2r  7917  inficl  8372  fipwss  8376  dffi3  8378  hartogslem1  8488  inf3lema  8559  inf3lemd  8562  cantnfle  8606  cantnflem2  8625  trcl  8642  tcmin  8655  rankr1ai  8699  rankxplim  8780  scottex  8786  scott0  8787  scottexs  8788  scott0s  8789  karden  8796  cardne  8829  cardaleph  8950  ackbij2  9103  cflim2  9123  cfslb  9126  coftr  9133  fin23lem15  9194  fin23lem32  9204  fin23lem34  9206  fin23lem35  9207  fin23lem36  9208  fin23lem41  9212  isf32lem1  9213  itunitc1  9280  axdc3lem2  9311  ttukeylem1  9369  fpwwe2cbv  9490  fpwwe2lem2  9492  fpwwe2  9503  fpwwecbv  9504  fpwwelem  9505  canthwelem  9510  canthwe  9511  wunex2  9598  wuncval2  9607  eltsk2g  9611  tskpwss  9612  inar1  9635  grothpw  9686  grothpwex  9687  axgroth6  9688  grothac  9690  peano5uzti  11505  fsuppmapnn0fiub0  12833  relexpnndm  13825  rtrclreclem4  13845  dfrtrcl2  13846  lo1o1  14307  o1lo1  14312  o1lo12  14313  lo1eq  14343  rlimeq  14344  isercoll  14442  prmreclem4  15670  vdwmc  15729  vdwlem1  15732  vdwlem2  15733  vdwlem12  15743  vdwlem13  15744  ramval  15759  ramz2  15775  ramub1lem1  15777  isacs2  16361  isacs1i  16365  mreacs  16366  acsfn  16367  rescabs  16540  ipole  17205  ipodrsima  17212  isacs5  17219  symgsssg  17933  psgnunilem5  17960  sylow1  18064  efgval2  18183  efgsfo  18198  frgpuplem  18231  gsumzf1o  18359  gsumzoppg  18390  dprdcntz  18453  islbs2  19202  frlmssuvc1  20181  frlmssuvc2  20182  frlmsslsp  20183  pptbas  20860  pnfnei  21072  mnfnei  21073  iscnp  21089  iscnp4  21115  cnntr  21127  cnconst2  21135  cnpresti  21140  cnprest  21141  isreg  21184  isnrm  21187  isnrm2  21210  perfcls  21217  isreg2  21229  hauscmplem  21257  1stcfb  21296  1stcelcls  21312  1stccnp  21313  txbas  21418  ptbasfi  21432  xkoopn  21440  xkoccn  21470  txcnp  21471  ptcnplem  21472  txdis  21483  txdis1cn  21486  txtube  21491  txkgen  21503  xkohaus  21504  xkoptsub  21505  xkoco1cn  21508  xkoco2cn  21509  xkococnlem  21510  xkococn  21511  xkoinjcn  21538  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  reghmph  21644  nrmhmph  21645  trfil2  21738  ufileu  21770  elfm  21798  elfm2  21799  elfm3  21801  imaelfm  21802  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  fmco  21812  elflim2  21815  flffbas  21846  lmflf  21856  txflf  21857  fclscf  21876  flimfnfcls  21879  cnextcn  21918  symgtgp  21952  ghmcnp  21965  qustgplem  21971  eltsms  21983  ustval  22053  ust0  22070  trust  22080  utoptop  22085  restutop  22088  restutopopn  22089  utopsnneiplem  22098  ucncn  22136  fmucnd  22143  cfilufg  22144  trcfilu  22145  neipcfilu  22147  blssps  22276  blss  22277  ssblex  22280  blin2  22281  metss2  22364  metrest  22376  metcnp3  22392  metustexhalf  22408  metustbl  22418  psmetutop  22419  xrsmopn  22662  recld2  22664  icccmplem1  22672  icccmplem2  22673  icccmp  22675  reconnlem2  22677  lebnumlem3  22809  lebnum  22810  xlebnum  22811  lebnumii  22812  nmhmcn  22966  cfilfval  23108  caubl  23152  caublcls  23153  bcthlem1  23167  bcth  23172  ovolfiniun  23315  ovoliunlem3  23318  ovoliun  23319  ovoliun2  23320  ovoliunnul  23321  voliunlem3  23366  dyadmax  23412  dyadmbllem  23413  dyadmbl  23414  opnmbllem  23415  ellimc2  23686  limcnlp  23687  ellimc3  23688  limcflf  23690  limciun  23703  cpnord  23743  lhop  23824  xrlimcnp  24740  cvxcl  24756  dchrval  25004  ausgrumgri  26107  ausgrusgri  26108  nbgrval  26274  nbgrel  26278  nbgrelOLD  26279  nbumgrvtx  26287  nbgrnself  26300  uvtxel1  26345  uvtxael1OLD  26347  wlkonl1iedg  26617  crctcshwlkn0lem6  26763  2wlkdlem10  26900  1wlkdlem4  27118  3wlkdlem6  27143  3wlkdlem10  27147  eupth2lem3lem4  27209  frcond1  27246  frgr1v  27251  nfrgr2v  27252  frgr3vlem1  27253  frgr3vlem2  27254  frgr3v  27255  4cycl2vnunb  27270  n4cyclfrgr  27271  isssp  27707  ubthlem1  27854  shmodi  28377  chsupid  28399  chsscon3  28487  spansncvi  28639  mdslmd1lem3  29314  mdslmd1lem4  29315  mdsymlem5  29394  dmdbr5ati  29409  dmdbr6ati  29410  dmdbr7ati  29411  ssiun2sf  29504  fpwrelmapffslem  29635  txomap  30029  locfinreflem  30035  tpr2rico  30086  pnfneige0  30125  rrhre  30193  prodindf  30213  dya2icoseg2  30468  omsfval  30484  eulerpartlemt0  30559  eulerpartgbij  30562  eulerpartlemr  30564  eulerpartlemgs2  30570  eulerpartlemn  30571  eulerpart  30572  bnj517  31081  bnj1014  31156  bnj1015  31157  bnj1123  31180  bnj1125  31186  bnj1450  31244  bnj1452  31246  kur14  31324  cvmliftlem15  31406  cvmlift2lem12  31422  cvmlift2lem13  31423  mclsval  31586  mclsax  31592  mclsppslem  31606  dfpo2  31771  trpredlem1  31851  trpredmintr  31855  frecseq123  31902  frrlem1  31905  frrlem3  31907  frrlem4  31908  frrlem5e  31913  noetalem5  31992  opnrebl  32440  opnrebl2  32441  ivthALT  32455  neibastop2lem  32480  fnemeet1  32486  filnetlem1  32498  filnetlem4  32501  csbwrecsg  33303  lindsenlbs  33534  ptrecube  33539  poimirlem32  33571  opnmbllem0  33575  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  ovoliunnfl  33581  ex-ovoliunnfl  33582  voliunnfl  33583  totbndbnd  33718  heibor1lem  33738  heiborlem10  33749  scottexf  34106  scott0f  34107  relcnveq2  34235  elrelscnveq2  34383  dfcnvrefrels2  34416  dfcnvrefrel2  34418  symrefref2  34447  lcv1  34646  lfl1dim  34726  lfl1dim2N  34727  paddasslem17  35440  dihglblem6  36946  dochvalr  36963  dochord3  36978  lpolconN  37093  lcfls1lem  37140  mapdffval  37232  mapdfval  37233  mapdsn2  37248  mapd0  37271  lspindp5  37376  mapdh8ab  37383  ismrcd1  37578  nacsfix  37592  setindtr  37908  hbtlem6  38016  clcnvlem  38247  iunrelexpmin1  38317  iunrelexpmin2  38321  relexp0a  38325  cotrcltrcl  38334  trclimalb2  38335  cotrclrcl  38351  sbcheg  38390  clsk1indlem1  38660  isotone1  38663  isotone2  38664  ntrclsiso  38682  ntrclsk2  38683  k0004lem1  38762  k0004lem3  38764  ssdec  39579  iinssd  39628  iinssdf  39642  ssnnf1octb  39696  iooiinicc  40087  iooiinioc  40101  icccncfext  40418  fourierdlem41  40683  meaiininclem  41021  hoidmvlelem3  41132  hoidmvle  41135  opnvonmbllem1  41167  opnvonmbl  41169  iinhoiicclem  41208  smflim  41306  smflimsuplem7  41353  uspgrsprf  42079  dfrngc2  42297  setrecseq  42757  setrec1lem4  42762  setrec2fun  42764
  Copyright terms: Public domain W3C validator