ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sseq1 GIF version

Theorem sseq1 2993
Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sseq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem sseq1
StepHypRef Expression
1 eqss 2987 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 2979 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 266 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 2979 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 265 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 124 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 118 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102   = wceq 1259  wss 2944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2951  df-ss 2958
This theorem is referenced by:  sseq12  2995  sseq1i  2996  sseq1d  2999  nssne2  3029  psseq1  3058  sspsstr  3077  sbss  3356  pwjust  3387  elpw  3392  elpwg  3394  sssnr  3551  ssprr  3554  sstpr  3555  unimax  3641  trss  3890  elssabg  3929  bnd2  3953  mss  3989  exss  3990  frforeq2  4109  ordtri2orexmid  4275  ontr2exmid  4277  onsucsssucexmid  4279  reg2exmidlema  4286  sucprcreg  4300  ordtri2or2exmid  4323  onintexmid  4324  tfis  4333  tfisi  4337  elnn  4355  nnregexmid  4369  releq  4449  xpsspw  4477  iss  4681  relcnvtr  4867  iotass  4911  fununi  4994  funcnvuni  4995  funimaexglem  5009  ffoss  5185  ssimaex  5261  tfrlem1  5953  nnsucsssuc  6101  qsss  6195  phpm  6357  ssfiexmid  6366  findcard2d  6378  findcard2sd  6379  diffifi  6381  elinp  6629  sumeq1  10104  bj-om  10427  bj-2inf  10428  bj-nntrans  10442  bj-omtrans  10447
  Copyright terms: Public domain W3C validator