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

Theorem sseq1 3088
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 3080 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3072 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 273 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3072 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 272 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 128 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 120 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1314  wss 3039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  sseq12  3090  sseq1i  3091  sseq1d  3094  nssne2  3124  sbss  3439  pwjust  3479  elpw  3484  elpwg  3486  sssnr  3648  ssprr  3651  sstpr  3652  unimax  3738  trss  4003  elssabg  4041  bnd2  4065  exmidexmid  4088  exmidsssn  4093  exmidsssnc  4094  mss  4116  exss  4117  frforeq2  4235  ordtri2orexmid  4406  ontr2exmid  4408  onsucsssucexmid  4410  reg2exmidlema  4417  sucprcreg  4432  ordtri2or2exmid  4454  onintexmid  4455  tfis  4465  tfisi  4469  elnn  4487  nnregexmid  4502  releq  4589  xpsspw  4619  iss  4833  relcnvtr  5026  iotass  5073  fununi  5159  funcnvuni  5160  funimaexglem  5174  ffoss  5365  ssimaex  5448  tfrlem1  6171  nnsucsssuc  6354  qsss  6454  phpm  6725  ssfiexmid  6736  findcard2d  6751  findcard2sd  6752  diffifi  6754  isinfinf  6757  fiintim  6783  fisseneq  6786  fidcenumlemrk  6808  fidcenumlemr  6809  sbthlem2  6812  isbth  6821  ctssdclemr  6963  elinp  7246  sup3exmid  8675  zfz1isolem1  10534  zfz1iso  10535  fimaxre2  10949  sumeq1  11075  fsum2d  11155  fsumabs  11185  fsumiun  11197  exmidunben  11845  ctiunct  11859  restsspw  12036  uniopn  12074  fiinopn  12077  fiinbas  12122  baspartn  12123  eltg2  12128  eltg3  12132  topbas  12142  clsval  12186  neival  12218  neiint  12220  neipsm  12229  opnneissb  12230  opnssneib  12231  innei  12238  restbasg  12243  cnpdis  12317  txbas  12333  eltx  12334  neitx  12343  txlm  12354  blssexps  12504  blssex  12505  neibl  12566  metrest  12581  xmettx  12585  tgioo  12621  tgqioo  12622  limcimolemlt  12708  recnprss  12731  bj-om  12969  bj-2inf  12970  bj-nntrans  12983  bj-omtrans  12988  el2oss1o  13022  exmid1stab  13029  subctctexmid  13030
  Copyright terms: Public domain W3C validator