Theorem dfpss2 2133

Description: Alternate definition of proper subclass.

Assertion

Ref	Expression
dfpss2	|- (A (. B <-> (A (_ B /\ -. A = B))

Proof of Theorem dfpss2

Step	Hyp	Ref	Expression
1		df-pss 2055	. 2 |- (A (. B <-> (A (_ B /\ A =/= B))
2		df-ne 1587	. . 3 |- (A =/= B <-> -. A = B)
3	2	anbi2i 480	. 2 |- ((A (_ B /\ A =/= B) <-> (A (_ B /\ -. A = B))
4	1, 3	bitr 173	1 |- (A (. B <-> (A (_ B /\ -. A = B))

Syntax hints:  -. wn 2   <-> wb 146   /\ wa 223   = wceq 956   =/= wne 1585   (_ wss 2047   (. wpss 2048

This theorem is referenced by:  dfpss3 2134  sspss 2145  psstr 2150  pssv 2310  disj4 2317  ssnelpss 2330  nnsdomo 4522  pssnn 4534  inf3lem6 4618  genpcl 5111  1pr 5117  ltaddpr 5140  chnle 9408  cvbr2t 10210  cvnbtwn2t 10214  cvnbtwn3t 10215  cvnbtwn4t 10216

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-ne 1587  df-pss 2055

Copyright terms: Public domain