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

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

Proof of Theorem sseq1
StepHypRef Expression
1 eqss 2937 . 2 (A = B ↔ (AB BA))
2 sstr2 2929 . . . 4 (BA → (A𝐶B𝐶))
32adantl 262 . . 3 ((AB BA) → (A𝐶B𝐶))
4 sstr2 2929 . . . 4 (AB → (B𝐶A𝐶))
54adantr 261 . . 3 ((AB BA) → (B𝐶A𝐶))
63, 5impbid 120 . 2 ((AB BA) → (A𝐶B𝐶))
71, 6sylbi 114 1 (A = B → (A𝐶B𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1228  wss 2894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908
This theorem is referenced by:  sseq12  2945  sseq1i  2946  sseq1d  2949  nssne2  2979  psseq1  3008  sspsstr  3027  sbss  3308  pwjust  3335  elpw  3340  elpwg  3342  sssnr  3498  ssprr  3501  sstpr  3502  unimax  3588  trss  3837  elssabg  3876  bnd2  3900  mss  3936  exss  3937  ordtri2orexmid  4195  onsucsssucexmid  4196  sucprcreg  4211  tfis  4233  tfisi  4237  elnn  4255  nnregexmid  4269  releq  4349  xpsspw  4377  iss  4581  relcnvtr  4767  iotass  4811  fununi  4893  funcnvuni  4894  funimaexglem  4908  ffoss  5083  ssimaex  5159  tfrlem1  5845  nnsucsssuc  5986  qsss  6076  elinp  6328  bj-om  7159  bj-2inf  7160  bj-nntrans  7173  bj-omtrans  7178
  Copyright terms: Public domain W3C validator