Theorem dfpss2 2136

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 2058	. 2 |- (A (. B <-> (A (_ B /\ A =/= B))
2		df-ne 1590	. . 3 |- (A =/= B <-> -. A = B)
3	2	anbi2i 482	. 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 958   =/= wne 1588   (_ wss 2050   (. wpss 2051

This theorem is referenced by:  dfpss3 2137  sspss 2148  psstr 2153  pssv 2314  disj4 2321  ssnelpss 2334  nnsdomo 4527  pssnn 4544  inf3lem6 4627  genpcl 5123  1pr 5129  ltaddpr 5152  chnle 9403  cvbr2t 10205  cvnbtwn2t 10209  cvnbtwn3t 10210  cvnbtwn4t 10211

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 1590  df-pss 2058

Copyright terms: Public domain