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

Theorem sseq1d 3794
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 3788 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  wss 3734
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3741  df-ss 3748
This theorem is referenced by:  sseq12d  3796  eqsstrd  3801  snssgOLD  4473  ssiun2s  4722  disjxiun  4808  treq  4919  iunopeqop  5144  preddowncl  5894  funimass1  6151  feq1  6206  fvmptss  6483  fvimacnvi  6523  fvimacnvALT  6528  knatar  6801  ovmptss  7462  fnsuppres  7527  imacosupp  7540  wrecseq123  7613  wfrlem1  7619  wfrlem3  7621  wfrdmcl  7629  wfrlem15  7635  wfrlem17  7637  dfrecs3  7675  oaordi  7833  oaword2  7840  oawordeulem  7841  omword1  7860  oewordri  7879  oeordsuc  7881  nnaordi  7905  nnawordex  7924  ereq1  7956  elpm2r  8080  inficl  8540  fipwss  8544  dffi3  8546  hartogslem1  8656  inf3lema  8738  inf3lemd  8741  cantnfle  8785  cantnflem2  8804  trcl  8821  tcmin  8834  rankr1ai  8878  rankxplim  8959  scottex  8965  scott0  8966  scottexs  8967  scott0s  8968  karden  8975  cardne  9044  cardaleph  9165  ackbij2  9320  cflim2  9340  cfslb  9343  coftr  9350  fin23lem15  9411  fin23lem32  9421  fin23lem34  9423  fin23lem35  9424  fin23lem36  9425  fin23lem41  9429  isf32lem1  9430  itunitc1  9497  axdc3lem2  9528  ttukeylem1  9586  fpwwe2cbv  9707  fpwwe2lem2  9709  fpwwe2  9720  fpwwecbv  9721  fpwwelem  9722  canthwelem  9727  canthwe  9728  wunex2  9815  wuncval2  9824  eltsk2g  9828  tskpwss  9829  inar1  9852  grothpw  9903  grothpwex  9904  axgroth6  9905  grothac  9907  peano5uzti  11717  fsuppmapnn0fiub0  13003  relexpnndm  14069  rtrclreclem4  14089  dfrtrcl2  14090  lo1o1  14551  o1lo1  14556  o1lo12  14557  lo1eq  14587  rlimeq  14588  isercoll  14686  prmreclem4  15905  vdwmc  15964  vdwlem1  15967  vdwlem2  15968  vdwlem12  15978  vdwlem13  15979  ramval  15994  ramz2  16010  ramub1lem1  16012  isacs2  16582  isacs1i  16586  mreacs  16587  acsfn  16588  rescabs  16761  ipole  17427  ipodrsima  17434  isacs5  17441  symgsssg  18153  psgnunilem5  18180  psgnunilem5OLD  18181  sylow1  18285  efgval2  18404  efgsfo  18420  frgpuplem  18454  gsumzf1o  18582  gsumzoppg  18613  dprdcntz  18677  islbs2  19431  frlmssuvc1  20412  frlmssuvc2  20413  frlmsslsp  20414  pptbas  21095  pnfnei  21307  mnfnei  21308  iscnp  21324  iscnp4  21350  cnntr  21362  cnconst2  21370  cnpresti  21375  cnprest  21376  isreg  21419  isnrm  21422  isnrm2  21445  perfcls  21452  isreg2  21464  hauscmplem  21492  1stcfb  21531  1stcelcls  21547  1stccnp  21548  txbas  21653  ptbasfi  21667  xkoopn  21675  xkoccn  21705  txcnp  21706  ptcnplem  21707  txdis  21718  txdis1cn  21721  txtube  21726  txkgen  21738  xkohaus  21739  xkoptsub  21740  xkoco1cn  21743  xkoco2cn  21744  xkococnlem  21745  xkococn  21746  xkoinjcn  21773  kqreglem1  21827  kqreglem2  21828  kqnrmlem1  21829  kqnrmlem2  21830  reghmph  21879  nrmhmph  21880  trfil2  21973  ufileu  22005  elfm  22033  elfm2  22034  elfm3  22036  imaelfm  22037  rnelfm  22039  fmfnfmlem2  22041  fmfnfmlem4  22043  fmco  22047  elflim2  22050  flffbas  22081  lmflf  22091  txflf  22092  fclscf  22111  flimfnfcls  22114  cnextcn  22153  symgtgp  22187  ghmcnp  22200  qustgplem  22206  eltsms  22218  ustval  22288  ust0  22305  trust  22315  utoptop  22320  restutop  22323  restutopopn  22324  utopsnneiplem  22333  ucncn  22371  fmucnd  22378  cfilufg  22379  trcfilu  22380  neipcfilu  22382  blssps  22511  blss  22512  ssblex  22515  blin2  22516  metss2  22599  metrest  22611  metcnp3  22627  metustexhalf  22643  metustbl  22653  psmetutop  22654  xrsmopn  22897  recld2  22899  icccmplem1  22907  icccmplem2  22908  icccmp  22910  reconnlem2  22912  lebnumlem3  23044  lebnum  23045  xlebnum  23046  lebnumii  23047  nmhmcn  23201  cfilfval  23344  caubl  23388  caublcls  23389  bcthlem1  23404  bcth  23409  ovolfiniun  23562  ovoliunlem3  23565  ovoliun  23566  ovoliun2  23567  ovoliunnul  23568  voliunlem3  23613  dyadmax  23659  dyadmbllem  23660  dyadmbl  23661  opnmbllem  23662  ellimc2  23935  limcnlp  23936  ellimc3  23937  limcflf  23939  limciun  23952  cpnord  23992  lhop  24073  xrlimcnp  24989  cvxcl  25005  dchrval  25253  ausgrumgri  26343  ausgrusgri  26344  nbgrval  26511  nbgrel  26515  nbgrelOLD  26516  nbumgrvtx  26524  nbgrnself  26537  uvtxel1  26583  uvtxael1OLD  26585  wlkonl1iedg  26855  crctcshwlkn0lem6  27003  2wlkdlem10  27161  1wlkdlem4  27421  3wlkdlem6  27446  3wlkdlem10  27450  eupth2lem3lem4  27512  frcond1  27549  frgr1v  27554  nfrgr2v  27555  frgr3vlem1  27556  frgr3vlem2  27557  frgr3v  27558  4cycl2vnunb  27573  n4cyclfrgr  27574  isssp  28038  ubthlem1  28185  shmodi  28708  chsupid  28730  chsscon3  28818  spansncvi  28970  mdslmd1lem3  29645  mdslmd1lem4  29646  mdsymlem5  29725  dmdbr5ati  29740  dmdbr6ati  29741  dmdbr7ati  29742  ssiun2sf  29829  fpwrelmapffslem  29959  txomap  30351  locfinreflem  30357  tpr2rico  30408  pnfneige0  30447  rrhre  30515  prodindf  30535  dya2icoseg2  30790  omsfval  30806  eulerpartlemt0  30881  eulerpartgbij  30884  eulerpartlemr  30886  eulerpartlemgs2  30892  eulerpartlemn  30893  eulerpart  30894  bnj517  31406  bnj1014  31481  bnj1015  31482  bnj1123  31505  bnj1125  31511  bnj1450  31569  bnj1452  31571  kur14  31649  cvmliftlem15  31731  cvmlift2lem12  31747  cvmlift2lem13  31748  mclsval  31911  mclsax  31917  mclsppslem  31931  dfpo2  32093  trpredlem1  32173  trpredmintr  32177  frecseq123  32224  frrlem1  32227  frrlem3  32229  frrlem4  32230  frrlem5e  32235  noetalem5  32314  opnrebl  32761  opnrebl2  32762  ivthALT  32776  neibastop2lem  32801  fnemeet1  32807  filnetlem1  32819  filnetlem4  32822  csbwrecsg  33610  lindsenlbs  33831  ptrecube  33836  poimirlem32  33868  opnmbllem0  33872  mblfinlem1  33873  mblfinlem2  33874  mblfinlem3  33875  ovoliunnfl  33878  ex-ovoliunnfl  33879  voliunnfl  33880  totbndbnd  34013  heibor1lem  34033  heiborlem10  34044  scottexf  34400  scott0f  34401  relcnveq2  34526  elrelscnveq2  34675  dfcnvrefrels2  34708  dfcnvrefrel2  34710  symrefref2  34741  lcv1  35000  lfl1dim  35080  lfl1dim2N  35081  paddasslem17  35795  dihglblem6  37299  dochvalr  37316  dochord3  37331  lpolconN  37446  lcfls1lem  37493  mapdffval  37585  mapdfval  37586  mapdsn2  37601  mapd0  37624  lspindp5  37729  mapdh8ab  37736  ismrcd1  37942  nacsfix  37956  setindtr  38271  hbtlem6  38379  clcnvlem  38608  iunrelexpmin1  38678  iunrelexpmin2  38682  relexp0a  38686  cotrcltrcl  38695  trclimalb2  38696  cotrclrcl  38712  sbcheg  38750  clsk1indlem1  39020  isotone1  39023  isotone2  39024  ntrclsiso  39042  ntrclsk2  39043  k0004lem1  39122  k0004lem3  39124  ssdec  39919  iinssd  39966  iinssdf  39980  ssnnf1octb  40032  iooiinicc  40410  iooiinioc  40424  icccncfext  40741  fourierdlem41  41005  meaiininclem  41343  hoidmvlelem3  41454  hoidmvle  41457  opnvonmbllem1  41489  opnvonmbl  41491  iinhoiicclem  41530  smflim  41628  smflimsuplem7  41675  uspgrsprf  42426  setrecseq  43104  setrec1lem4  43109  setrec2fun  43111
  Copyright terms: Public domain W3C validator