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

Theorem sseq1d 4002
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 3996 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wss 3940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-in 3947  df-ss 3956
This theorem is referenced by:  sseq12d  4004  eqsstrd  4009  ssiun2s  4969  disjxiun  5060  treq  5175  iunopeqop  5408  preddowncl  6173  funimass1  6433  feq1  6492  fvmptss  6776  fvimacnvi  6818  fvimacnvALT  6823  knatar  7102  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  18515  psgnunilem5  18542  sylow1  18648  efgval2  18770  efgsfo  18785  frgpuplem  18818  gsumzf1o  18952  gsumzoppg  18984  dprdcntz  19050  islbs2  19846  ismhp  20251  frlmssuvc1  20854  frlmssuvc2  20855  frlmsslsp  20856  pptbas  21532  pnfnei  21744  mnfnei  21745  iscnp  21761  iscnp4  21787  cnntr  21799  cnconst2  21807  cnpresti  21812  cnprest  21813  isreg  21856  isnrm  21859  isnrm2  21882  perfcls  21889  isreg2  21901  hauscmplem  21930  1stcfb  21969  1stcelcls  21985  1stccnp  21986  txbas  22091  ptbasfi  22105  xkoopn  22113  xkoccn  22143  txcnp  22144  ptcnplem  22145  txdis  22156  txdis1cn  22159  txtube  22164  txkgen  22176  xkohaus  22177  xkoptsub  22178  xkoco1cn  22181  xkoco2cn  22182  xkococnlem  22183  xkococn  22184  xkoinjcn  22211  kqreglem1  22265  kqreglem2  22266  kqnrmlem1  22267  kqnrmlem2  22268  reghmph  22317  nrmhmph  22318  trfil2  22411  ufileu  22443  elfm  22471  elfm2  22472  elfm3  22474  imaelfm  22475  rnelfm  22477  fmfnfmlem2  22479  fmfnfmlem4  22481  fmco  22485  elflim2  22488  flffbas  22519  lmflf  22529  txflf  22530  fclscf  22549  flimfnfcls  22552  cnextcn  22591  symgtgp  22625  ghmcnp  22638  qustgplem  22644  eltsms  22656  ustval  22726  ust0  22743  trust  22753  utoptop  22758  restutop  22761  restutopopn  22762  utopsnneiplem  22771  ucncn  22809  fmucnd  22816  cfilufg  22817  trcfilu  22818  neipcfilu  22820  blssps  22949  blss  22950  ssblex  22953  blin2  22954  metss2  23037  metrest  23049  metcnp3  23065  metustexhalf  23081  metustbl  23091  psmetutop  23092  xrsmopn  23335  recld2  23337  icccmplem1  23345  icccmplem2  23346  icccmp  23348  reconnlem2  23350  lebnumlem3  23482  lebnum  23483  xlebnum  23484  lebnumii  23485  nmhmcn  23639  cfilfval  23782  caubl  23826  caublcls  23827  bcthlem1  23842  bcth  23847  ovolfiniun  24017  ovoliunlem3  24020  ovoliun  24021  ovoliun2  24022  ovoliunnul  24023  voliunlem3  24068  dyadmax  24114  dyadmbllem  24115  dyadmbl  24116  opnmbllem  24117  ellimc2  24390  limcnlp  24391  ellimc3  24392  limcflf  24394  limciun  24407  cpnord  24447  lhop  24528  xrlimcnp  25460  cvxcl  25476  dchrval  25724  ausgrumgri  26866  ausgrusgri  26867  nbgrval  27032  nbgrel  27036  nbumgrvtx  27042  nbgrnself  27055  uvtxel1  27092  wlkonl1iedg  27361  crctcshwlkn0lem6  27507  2wlkdlem10  27628  1wlkdlem4  27833  3wlkdlem6  27858  3wlkdlem10  27862  eupth2lem3lem4  27924  frcond1  27959  frgr1v  27964  nfrgr2v  27965  frgr3vlem1  27966  frgr3vlem2  27967  frgr3v  27968  4cycl2vnunb  27983  n4cyclfrgr  27984  isssp  28415  ubthlem1  28561  shmodi  29081  chsupid  29103  chsscon3  29191  spansncvi  29343  mdslmd1lem3  30018  mdslmd1lem4  30019  mdsymlem5  30098  dmdbr5ati  30113  dmdbr6ati  30114  dmdbr7ati  30115  ssiun2sf  30226  fpwrelmapffslem  30381  txomap  30984  locfinreflem  30990  tpr2rico  31041  pnfneige0  31080  rrhre  31148  prodindf  31168  dya2icoseg2  31422  omsfval  31438  eulerpartlemt0  31513  eulerpartgbij  31516  eulerpartlemr  31518  eulerpartlemgs2  31524  eulerpartlemn  31525  eulerpart  31526  bnj517  32043  bnj1014  32118  bnj1015  32119  bnj1123  32142  bnj1125  32148  bnj1450  32206  bnj1452  32208  cplgredgex  32251  kur14  32347  cvmliftlem15  32429  cvmlift2lem12  32445  cvmlift2lem13  32446  mclsval  32694  mclsax  32700  mclsppslem  32714  dfpo2  32875  trpredlem1  32950  trpredmintr  32954  frecseq123  33003  frrlem1  33007  frrlem3  33009  frrlem4  33010  frrlem13  33019  noetalem5  33105  opnrebl  33552  opnrebl2  33553  ivthALT  33567  neibastop2lem  33592  fnemeet1  33598  filnetlem1  33610  filnetlem4  33613  bj-imdirval3  34353  csbwrecsg  34477  rdgssun  34528  lindsadd  34752  lindsenlbs  34754  ptrecube  34759  poimirlem32  34791  opnmbllem0  34795  mblfinlem1  34796  mblfinlem2  34797  mblfinlem3  34798  ovoliunnfl  34801  ex-ovoliunnfl  34802  voliunnfl  34803  totbndbnd  34935  heibor1lem  34955  heiborlem10  34966  scottexf  35314  scott0f  35315  relcnveq2  35448  elrelscnveq2  35600  dfcnvrefrels2  35633  dfcnvrefrel2  35635  symrefref2  35666  lcv1  36044  lfl1dim  36124  lfl1dim2N  36125  paddasslem17  36839  dihglblem6  38343  dochvalr  38360  dochord3  38375  lpolconN  38490  lcfls1lem  38537  mapdffval  38629  mapdfval  38630  mapdsn2  38645  mapd0  38668  lspindp5  38773  mapdh8ab  38780  ismrcd1  39160  nacsfix  39174  setindtr  39486  hbtlem6  39594  clcnvlem  39848  iunrelexpmin1  39918  iunrelexpmin2  39922  relexp0a  39926  cotrcltrcl  39935  trclimalb2  39936  cotrclrcl  39952  sbcheg  39990  clsk1indlem1  40260  isotone1  40263  isotone2  40264  ntrclsiso  40282  ntrclsk2  40283  k0004lem1  40362  k0004lem3  40364  scottelrankd  40448  mnuop123d  40463  mnuprdlem1  40473  mnuprdlem2  40474  mnuunid  40478  mnurndlem1  40482  ssdec  41219  iinssd  41262  iinssdf  41273  ssnnf1octb  41321  iooiinicc  41683  iooiinioc  41697  icccncfext  42035  fourierdlem41  42299  meaiininclem  42634  hoidmvlelem3  42745  hoidmvle  42748  opnvonmbllem1  42780  opnvonmbl  42782  iinhoiicclem  42821  smflim  42919  smflimsuplem7  42966  uspgrsprf  43853  setrecseq  44620  setrec1lem4  44625  setrec2fun  44627
  Copyright terms: Public domain W3C validator