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

Theorem sseq2 2994
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 2979 . . . 4 (𝐶𝐴 → (𝐴𝐵𝐶𝐵))
21com12 30 . . 3 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
3 sstr2 2979 . . . 4 (𝐶𝐵 → (𝐵𝐴𝐶𝐴))
43com12 30 . . 3 (𝐵𝐴 → (𝐶𝐵𝐶𝐴))
52, 4anim12i 325 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
6 eqss 2987 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
7 dfbi2 374 . 2 ((𝐶𝐴𝐶𝐵) ↔ ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
85, 6, 73imtr4i 194 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102   = wceq 1259  wss 2944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2951  df-ss 2958
This theorem is referenced by:  sseq12  2995  sseq2i  2997  sseq2d  3000  syl5sseq  3020  nssne1  3028  psseq2  3059  sseq0  3285  un00  3290  disjpss  3305  pweq  3389  ssintab  3659  ssintub  3660  intmin  3662  treq  3887  ssexg  3923  frforeq3  4111  frirrg  4114  iunpw  4238  ordtri2orexmid  4275  ontr2exmid  4277  onsucsssucexmid  4279  ordtri2or2exmid  4323  fununi  4994  funcnvuni  4995  feq3  5059  ssimaexg  5262  nnawordex  6131  ereq1  6143  xpiderm  6207  domeng  6263  ssfiexmid  6366  bdssexg  10397  bj-nntrans  10449  bj-omtrans  10454
  Copyright terms: Public domain W3C validator