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

Theorem sseq1 3031
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 3025 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3017 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 271 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3017 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 270 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 127 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 119 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wss 2984
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2990  df-ss 2997
This theorem is referenced by:  sseq12  3033  sseq1i  3034  sseq1d  3037  nssne2  3067  sbss  3371  pwjust  3407  elpw  3412  elpwg  3414  sssnr  3571  ssprr  3574  sstpr  3575  unimax  3661  trss  3910  elssabg  3949  bnd2  3973  exmidexmid  3995  mss  4017  exss  4018  frforeq2  4136  ordtri2orexmid  4302  ontr2exmid  4304  onsucsssucexmid  4306  reg2exmidlema  4313  sucprcreg  4328  ordtri2or2exmid  4350  onintexmid  4351  tfis  4361  tfisi  4365  elnn  4383  nnregexmid  4397  releq  4478  xpsspw  4508  iss  4715  relcnvtr  4904  iotass  4951  fununi  5035  funcnvuni  5036  funimaexglem  5050  ffoss  5233  ssimaex  5310  tfrlem1  6005  nnsucsssuc  6185  qsss  6281  phpm  6511  ssfiexmid  6522  findcard2d  6537  findcard2sd  6538  diffifi  6540  isinfinf  6543  fisseneq  6567  elinp  6936  fimaxre2  10483  sumeq1  10566  bj-om  11175  bj-2inf  11176  bj-nntrans  11189  bj-omtrans  11194  el2oss1o  11230
  Copyright terms: Public domain W3C validator