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

Theorem sseq2 2944
 Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
sseq2 (A = B → (𝐶A𝐶B))

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 2929 . . . 4 (𝐶A → (AB𝐶B))
21com12 27 . . 3 (AB → (𝐶A𝐶B))
3 sstr2 2929 . . . 4 (𝐶B → (BA𝐶A))
43com12 27 . . 3 (BA → (𝐶B𝐶A))
52, 4anim12i 321 . 2 ((AB BA) → ((𝐶A𝐶B) (𝐶B𝐶A)))
6 eqss 2937 . 2 (A = B ↔ (AB BA))
7 dfbi2 368 . 2 ((𝐶A𝐶B) ↔ ((𝐶A𝐶B) (𝐶B𝐶A)))
85, 6, 73imtr4i 190 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  sseq2i  2947  sseq2d  2950  syl5sseq  2970  nssne1  2978  psseq2  3009  sseq0  3235  un00  3240  disjpss  3255  pweq  3337  ssintab  3606  ssintub  3607  intmin  3609  treq  3834  ssexg  3870  iunpw  4161  ordtri2orexmid  4195  onsucsssucexmid  4196  fununi  4893  funcnvuni  4894  feq3  4958  ssimaexg  5160  nnawordex  6012  ereq1  6024  xpiderm  6088  bdssexg  7127  bj-nntrans  7173  bj-omtrans  7178
 Copyright terms: Public domain W3C validator