Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sspred Structured version   Unicode version

Theorem sspred 29179
 Description: Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011.)
Assertion
Ref Expression
sspred

Proof of Theorem sspred
StepHypRef Expression
1 sseqin2 3722 . 2
2 df-pred 29171 . . . 4
32sseq1i 3533 . . 3
4 df-ss 3495 . . 3
5 in32 3715 . . . 4
65eqeq1i 2474 . . 3
73, 4, 63bitri 271 . 2
8 ineq1 3698 . . . . 5
98eqeq1d 2469 . . . 4
109biimpa 484 . . 3
11 df-pred 29171 . . . . . 6
122, 11eqeq12i 2487 . . . . 5
1312biimpri 206 . . . 4
1413eqcoms 2479 . . 3
1510, 14syl 16 . 2
161, 7, 15syl2anb 479 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   cin 3480   wss 3481  csn 4033  ccnv 5004  cima 5008  cpred 29170 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-in 3488  df-ss 3495  df-pred 29171 This theorem is referenced by:  frmin  29249
 Copyright terms: Public domain W3C validator