Theorem dfpss3 3693

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
dfpss3	|- ( A C. B <-> ( A C_ B /\ -. B C_ A ) )

Proof of Theorem dfpss3

Step	Hyp	Ref	Expression
1		dfpss2 3692	. 2 |- ( A C. B <-> ( A C_ B /\ -. A = B ) )
2		eqss 3618	. . . . 5 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
3	2	baib 944	. . . 4 |- ( A C_ B -> ( A = B <-> B C_ A ) )
4	3	notbid 308	. . 3 |- ( A C_ B -> ( -. A = B <-> -. B C_ A ) )
5	4	pm5.32i 669	. 2 |- ( ( A C_ B /\ -. A = B ) <-> ( A C_ B /\ -. B C_ A ) )
6	1, 5	bitri 264	1 |- ( A C. B <-> ( A C_ B /\ -. B C_ A ) )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   = wceq 1483   C_ wss 3574   C. wpss 3575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ne 2795  df-in 3581  df-ss 3588  df-pss 3590

This theorem is referenced by:  pssirr  3707  pssn2lp  3708  ssnpss  3710  nsspssun  3857  npss0OLD  4015  pssdifcom1  4054  pssdifcom2  4055  php3  8146  fincssdom  9145  reclem2pr  9870  ressval3d  15937  islbs3  19155  chpsscon3  28362  chpssati  29222  fundmpss  31664  lpssat  34300  lssat  34303  dihglblem6  36629  pssnssi  39283  mbfpsssmf  40991