Theorem sspss 3602

Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.)

Assertion

Ref	Expression
sspss

Proof of Theorem sspss

Step	Hyp	Ref	Expression
1		dfpss2 3588	. . . . 5
2	1	simplbi2 625	. . . 4
3	2	con1d 124	. . 3
4	3	orrd 378	. 2
5		pssss 3598	. . 3
6		eqimss 3555	. . 3
7	5, 6	jaoi 379	. 2
8	4, 7	impbii 188	1

Syntax hints:  -.wn 3  <->wb 184  \/wo 368  =wceq 1395  C_wss 3475  C.wpss 3476

This theorem is referenced by:  sspsstri  3605  sspsstr  3608  psssstr  3609  ordsseleq  4912  sorpssuni  6589  sorpssint  6590  ssnnfi  7759  ackbij1b  8640  fin23lem40  8752  zorng  8905  psslinpr  9430  suplem2pr  9452  mrissmrcd  15037  pgpssslw  16634  pgpfac1lem5  17130  idnghm  21250  dfon2lem4  29218  finminlem  30136  ressval3d  32558  lkrss2N  34894  dvh3dim3N  37176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ne 2654  df-in 3482  df-ss 3489  df-pss 3491