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

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

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 3021 . . . 4 (𝐶𝐴 → (𝐴𝐵𝐶𝐵))
21com12 30 . . 3 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
3 sstr2 3021 . . . 4 (𝐶𝐵 → (𝐵𝐴𝐶𝐴))
43com12 30 . . 3 (𝐵𝐴 → (𝐶𝐵𝐶𝐴))
52, 4anim12i 331 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
6 eqss 3029 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
7 dfbi2 380 . 2 ((𝐶𝐴𝐶𝐵) ↔ ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
85, 6, 73imtr4i 199 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1287  wss 2988
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001
This theorem is referenced by:  sseq12  3038  sseq2i  3040  sseq2d  3043  syl5sseq  3063  nssne1  3071  sseq0  3312  un00  3317  pweq  3418  ssintab  3688  ssintub  3689  intmin  3691  treq  3917  ssexg  3953  exmidundif  4009  frforeq3  4148  frirrg  4151  iunpw  4275  ordtri2orexmid  4312  ontr2exmid  4314  onsucsssucexmid  4316  ordtri2or2exmid  4360  fununi  5047  funcnvuni  5048  feq3  5112  ssimaexg  5329  nnawordex  6239  ereq1  6251  xpiderm  6315  domeng  6421  ssfiexmid  6544  fisseneq  6592  sbthlemi4  6613  sbthlemi5  6614  bdssexg  11240  bj-nntrans  11291  bj-omtrans  11296
  Copyright terms: Public domain W3C validator