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

Theorem sseq2i 3993
Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
sseq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
sseq2i (𝐶𝐴𝐶𝐵)

Proof of Theorem sseq2i
StepHypRef Expression
1 sseq1i.1 . 2 𝐴 = 𝐵
2 sseq2 3990 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  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:  sseqtri  4000  sseqtrdi  4014  abss  4037  ssrab  4046  ssindif0  4409  difcom  4430  ssunsn2  4752  ssunpr  4757  sspr  4758  sstp  4759  ssintrab  4890  iunpwss  5020  propssopi  5389  dffun2  6358  ssimaex  6741  elpwun  7480  frfi  8751  alephislim  9497  cardaleph  9503  fin1a2lem12  9821  zornn0g  9915  ssxr  10698  nnwo  12301  isstruct  16484  issubm  17956  grpissubg  18237  islinds  20881  basdif0  21489  tgdif0  21528  cmpsublem  21935  cmpsub  21936  hauscmplem  21942  2ndcctbss  21991  fbncp  22375  cnextfval  22598  eltsms  22668  reconn  23363  cmssmscld  23880  axcontlem3  26679  axcontlem4  26680  umgredg  26850  nbuhgr  27052  uhgrvd00  27243  vtxdginducedm1  27252  chsscon1i  29166  hatomistici  30066  chirredlem4  30097  atabs2i  30106  mdsymlem1  30107  mdsymlem3  30109  mdsymlem6  30112  mdsymlem8  30114  dmdbr5ati  30126  iundifdif  30242  nocvxminlem  33144  nocvxmin  33145  poimir  34806  ismblfin  34814  cossssid2  35588  ntrk0kbimka  40267  ntrclsk3  40298  ntrneicls11  40318  abssf  41255  ssrabf  41258  stoweidlem57  42219  ovnsubadd  42731  ovnovollem3  42817  issubmgm  43933  linccl  44397  lincdifsn  44407
  Copyright terms: Public domain W3C validator