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

Theorem sseq2i 3622
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 3619 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1481  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  sseqtri  3629  syl6sseq  3643  abss  3663  ssrab  3672  ssindif0  4022  difcom  4044  ssunsn2  4350  ssunpr  4356  sspr  4357  sstp  4358  ssintrab  4491  iunpwss  4609  propssopi  4961  dffun2  5886  ssimaex  6250  elpwun  6962  frfi  8190  alephislim  8891  cardaleph  8897  fin1a2lem12  9218  zornn0g  9312  ssxr  10092  nnwo  11738  isstruct  15851  issubm  17328  grpissubg  17595  islinds  20129  basdif0  20738  tgdif0  20777  cmpsublem  21183  cmpsub  21184  hauscmplem  21190  2ndcctbss  21239  fbncp  21624  cnextfval  21847  eltsms  21917  reconn  22612  axcontlem3  25827  axcontlem4  25828  umgredg  26014  nbuhgr  26220  uhgrvd00  26411  vtxdginducedm1  26420  chsscon1i  28291  hatomistici  29191  chirredlem4  29222  atabs2i  29231  mdsymlem1  29232  mdsymlem3  29234  mdsymlem6  29237  mdsymlem8  29239  dmdbr5ati  29251  iundifdif  29353  nocvxminlem  31867  nocvxmin  31868  poimir  33413  ismblfin  33421  ntrk0kbimka  38157  ntrclsk3  38188  ntrneicls11  38208  abssf  39115  ssrabf  39118  stoweidlem57  40037  ovnsubadd  40549  ovnovollem3  40635  issubmgm  41554  linccl  41968  lincdifsn  41978
  Copyright terms: Public domain W3C validator