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

Theorem sseq1 3179
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 3171 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3163 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 277 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3163 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 276 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 129 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 121 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wss 3130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143
This theorem is referenced by:  sseq12  3181  sseq1i  3182  sseq1d  3185  nssne2  3215  sbss  3532  pwjust  3577  elpw  3582  elpwg  3584  sssnr  3754  ssprr  3757  sstpr  3758  unimax  3844  trss  4111  elssabg  4149  bnd2  4174  exmidexmid  4197  exmidsssn  4203  exmidsssnc  4204  exmid1stab  4209  mss  4227  exss  4228  frforeq2  4346  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  reg2exmidlema  4534  sucprcreg  4549  ordtri2or2exmid  4571  ontri2orexmidim  4572  onintexmid  4573  tfis  4583  tfisi  4587  elomssom  4605  nnregexmid  4621  releq  4709  xpsspw  4739  iss  4954  relcnvtr  5149  iotass  5196  fununi  5285  funcnvuni  5286  funimaexglem  5300  ffoss  5494  ssimaex  5578  tfrlem1  6309  el2oss1o  6444  nnsucsssuc  6493  qsss  6594  phpm  6865  ssfiexmid  6876  findcard2d  6891  findcard2sd  6892  diffifi  6894  isinfinf  6897  fiintim  6928  fisseneq  6931  fidcenumlemrk  6953  fidcenumlemr  6954  sbthlem2  6957  isbth  6966  ctssdclemr  7111  onntri45  7240  tapeq1  7251  elinp  7473  sup3exmid  8914  zfz1isolem1  10820  zfz1iso  10821  fimaxre2  11235  sumeq1  11363  fsum2d  11443  fsumabs  11473  fsumiun  11485  prodeq1f  11560  fprod2d  11631  exmidunben  12427  ctiunct  12441  ssomct  12446  restsspw  12698  uniopn  13504  fiinopn  13507  fiinbas  13552  baspartn  13553  eltg2  13556  eltg3  13560  topbas  13570  clsval  13614  neival  13646  neiint  13648  neipsm  13657  opnneissb  13658  opnssneib  13659  innei  13666  restbasg  13671  cnpdis  13745  txbas  13761  eltx  13762  neitx  13771  txlm  13782  blssexps  13932  blssex  13933  neibl  13994  metrest  14009  xmettx  14013  tgioo  14049  tgqioo  14050  limcimolemlt  14136  recnprss  14159  bj-om  14692  bj-2inf  14693  bj-nntrans  14706  bj-omtrans  14711  subctctexmid  14753  pw1nct  14755
  Copyright terms: Public domain W3C validator