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

Theorem sseq1d 3997
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 3991 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wss 3935
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  sseq12d  3999  eqsstrd  4004  ssiun2s  4964  disjxiun  5055  treq  5170  iunopeqop  5403  preddowncl  6169  funimass1  6430  feq1  6489  fvmptss  6773  fvimacnvi  6815  fvimacnvALT  6820  knatar  7099  ovmptss  7779  fnsuppres  7848  imacosuppOLD  7866  wrecseq123  7939  wfrlem1  7945  wfrlem3  7947  wfrdmcl  7954  wfrlem15  7960  wfrlem17  7962  dfrecs3  8000  oaordi  8162  oaword2  8169  oawordeulem  8170  omword1  8189  oewordri  8208  oeordsuc  8210  nnaordi  8234  nnawordex  8253  ereq1  8286  elpm2r  8414  inficl  8878  fipwss  8882  dffi3  8884  hartogslem1  8995  inf3lema  9076  inf3lemd  9079  cantnfle  9123  cantnflem2  9142  trcl  9159  tcmin  9172  rankr1ai  9216  rankxplim  9297  scottex  9303  scott0  9304  scottexs  9305  scott0s  9306  karden  9313  cardne  9383  cardaleph  9504  ackbij2  9654  cflim2  9674  cfslb  9677  coftr  9684  fin23lem15  9745  fin23lem32  9755  fin23lem34  9757  fin23lem35  9758  fin23lem36  9759  fin23lem41  9763  isf32lem1  9764  itunitc1  9831  axdc3lem2  9862  ttukeylem1  9920  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwe2  10054  fpwwecbv  10055  fpwwelem  10056  canthwelem  10061  canthwe  10062  wunex2  10149  wuncval2  10158  eltsk2g  10162  tskpwss  10163  inar1  10186  grothpw  10237  grothpwex  10238  axgroth6  10239  grothac  10241  peano5uzti  12061  fsuppmapnn0fiub0  13351  relexpnndm  14390  rtrclreclem4  14410  dfrtrcl2  14411  lo1o1  14879  o1lo1  14884  o1lo12  14885  lo1eq  14915  rlimeq  14916  isercoll  15014  prmreclem4  16245  vdwmc  16304  vdwlem1  16307  vdwlem2  16308  vdwlem12  16318  vdwlem13  16319  ramval  16334  ramz2  16350  ramub1lem1  16352  isacs2  16914  isacs1i  16918  mreacs  16919  acsfn  16920  rescabs  17093  ipole  17758  ipodrsima  17765  isacs5  17772  symgsssg  18526  psgnunilem5  18553  sylow1  18659  efgval2  18781  efgsfo  18796  frgpuplem  18829  gsumzf1o  18963  gsumzoppg  18995  dprdcntz  19061  islbs2  19857  ismhp  20264  frlmssuvc1  20868  frlmssuvc2  20869  frlmsslsp  20870  pptbas  21546  pnfnei  21758  mnfnei  21759  iscnp  21775  iscnp4  21801  cnntr  21813  cnconst2  21821  cnpresti  21826  cnprest  21827  isreg  21870  isnrm  21873  isnrm2  21896  perfcls  21903  isreg2  21915  hauscmplem  21944  1stcfb  21983  1stcelcls  21999  1stccnp  22000  txbas  22105  ptbasfi  22119  xkoopn  22127  xkoccn  22157  txcnp  22158  ptcnplem  22159  txdis  22170  txdis1cn  22173  txtube  22178  txkgen  22190  xkohaus  22191  xkoptsub  22192  xkoco1cn  22195  xkoco2cn  22196  xkococnlem  22197  xkococn  22198  xkoinjcn  22225  kqreglem1  22279  kqreglem2  22280  kqnrmlem1  22281  kqnrmlem2  22282  reghmph  22331  nrmhmph  22332  trfil2  22425  ufileu  22457  elfm  22485  elfm2  22486  elfm3  22488  imaelfm  22489  rnelfm  22491  fmfnfmlem2  22493  fmfnfmlem4  22495  fmco  22499  elflim2  22502  flffbas  22533  lmflf  22543  txflf  22544  fclscf  22563  flimfnfcls  22566  cnextcn  22605  symgtgp  22639  ghmcnp  22652  qustgplem  22658  eltsms  22670  ustval  22740  ust0  22757  trust  22767  utoptop  22772  restutop  22775  restutopopn  22776  utopsnneiplem  22785  ucncn  22823  fmucnd  22830  cfilufg  22831  trcfilu  22832  neipcfilu  22834  blssps  22963  blss  22964  ssblex  22967  blin2  22968  metss2  23051  metrest  23063  metcnp3  23079  metustexhalf  23095  metustbl  23105  psmetutop  23106  xrsmopn  23349  recld2  23351  icccmplem1  23359  icccmplem2  23360  icccmp  23362  reconnlem2  23364  lebnumlem3  23496  lebnum  23497  xlebnum  23498  lebnumii  23499  nmhmcn  23653  cfilfval  23796  caubl  23840  caublcls  23841  bcthlem1  23856  bcth  23861  ovolfiniun  24031  ovoliunlem3  24034  ovoliun  24035  ovoliun2  24036  ovoliunnul  24037  voliunlem3  24082  dyadmax  24128  dyadmbllem  24129  dyadmbl  24130  opnmbllem  24131  ellimc2  24404  limcnlp  24405  ellimc3  24406  limcflf  24408  limciun  24421  cpnord  24461  lhop  24542  xrlimcnp  25474  cvxcl  25490  dchrval  25738  ausgrumgri  26880  ausgrusgri  26881  nbgrval  27046  nbgrel  27050  nbumgrvtx  27056  nbgrnself  27069  uvtxel1  27106  wlkonl1iedg  27375  crctcshwlkn0lem6  27521  2wlkdlem10  27642  1wlkdlem4  27847  3wlkdlem6  27872  3wlkdlem10  27876  eupth2lem3lem4  27938  frcond1  27973  frgr1v  27978  nfrgr2v  27979  frgr3vlem1  27980  frgr3vlem2  27981  frgr3v  27982  4cycl2vnunb  27997  n4cyclfrgr  27998  isssp  28429  ubthlem1  28575  shmodi  29095  chsupid  29117  chsscon3  29205  spansncvi  29357  mdslmd1lem3  30032  mdslmd1lem4  30033  mdsymlem5  30112  dmdbr5ati  30127  dmdbr6ati  30128  dmdbr7ati  30129  ssiun2sf  30240  fpwrelmapffslem  30395  txomap  30998  locfinreflem  31004  tpr2rico  31055  pnfneige0  31094  rrhre  31162  prodindf  31182  dya2icoseg2  31436  omsfval  31452  eulerpartlemt0  31527  eulerpartgbij  31530  eulerpartlemr  31532  eulerpartlemgs2  31538  eulerpartlemn  31539  eulerpart  31540  bnj517  32057  bnj1014  32132  bnj1015  32133  bnj1123  32156  bnj1125  32162  bnj1450  32220  bnj1452  32222  cplgredgex  32265  kur14  32361  cvmliftlem15  32443  cvmlift2lem12  32459  cvmlift2lem13  32460  mclsval  32708  mclsax  32714  mclsppslem  32728  dfpo2  32889  trpredlem1  32964  trpredmintr  32968  frecseq123  33017  frrlem1  33021  frrlem3  33023  frrlem4  33024  frrlem13  33033  noetalem5  33119  opnrebl  33566  opnrebl2  33567  ivthALT  33581  neibastop2lem  33606  fnemeet1  33612  filnetlem1  33624  filnetlem4  33627  bj-imdirval3  34367  csbwrecsg  34491  rdgssun  34542  lindsadd  34767  lindsenlbs  34769  ptrecube  34774  poimirlem32  34806  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  mblfinlem3  34813  ovoliunnfl  34816  ex-ovoliunnfl  34817  voliunnfl  34818  totbndbnd  34950  heibor1lem  34970  heiborlem10  34981  scottexf  35329  scott0f  35330  relcnveq2  35463  elrelscnveq2  35615  dfcnvrefrels2  35648  dfcnvrefrel2  35650  symrefref2  35681  lcv1  36059  lfl1dim  36139  lfl1dim2N  36140  paddasslem17  36854  dihglblem6  38358  dochvalr  38375  dochord3  38390  lpolconN  38505  lcfls1lem  38552  mapdffval  38644  mapdfval  38645  mapdsn2  38660  mapd0  38683  lspindp5  38788  mapdh8ab  38795  ismrcd1  39175  nacsfix  39189  setindtr  39501  hbtlem6  39609  clcnvlem  39863  iunrelexpmin1  39933  iunrelexpmin2  39937  relexp0a  39941  cotrcltrcl  39950  trclimalb2  39951  cotrclrcl  39967  sbcheg  40005  clsk1indlem1  40275  isotone1  40278  isotone2  40279  ntrclsiso  40297  ntrclsk2  40298  k0004lem1  40377  k0004lem3  40379  scottelrankd  40463  mnuop123d  40478  mnuprdlem1  40488  mnuprdlem2  40489  mnuunid  40493  mnurndlem1  40497  ssdec  41234  iinssd  41277  iinssdf  41288  ssnnf1octb  41336  iooiinicc  41698  iooiinioc  41712  icccncfext  42050  fourierdlem41  42314  meaiininclem  42649  hoidmvlelem3  42760  hoidmvle  42763  opnvonmbllem1  42795  opnvonmbl  42797  iinhoiicclem  42836  smflim  42934  smflimsuplem7  42981  uspgrsprf  43868  setrecseq  44686  setrec1lem4  44691  setrec2fun  44693
  Copyright terms: Public domain W3C validator