Theorem dfpss2 1557

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 1494	. 2 |- (A (. B <-> (A (_ B /\ A =/= B))
2		df-ne 1192	. . 3 |- (A =/= B <-> -. A = B)
3	2	anbi2i 367	. 2 |- ((A (_ B /\ A =/= B) <-> (A (_ B /\ -. A = B))
4	1, 3	bitr 151	1 |- (A (. B <-> (A (_ B /\ -. A = B))

Syntax hints:  -. wn 1   <-> wb 127   /\ wa 196   = wceq 1091   =/= wne 1190   (_ wss 1487   (. wpss 1488

This theorem is referenced by:  dfpss3 1558  sspss 1569  psstr 1574  0pss 1730  pssv 1732  disj4 1737  ssnelpss 1751  pssnel 1752  ordelpss 2226  nnsdomo 3417  ominf 3423  pssnn 3428  inf3lem2 3465  inf3lem4 3467  inf3lem6 3469  inf5 3472  genpcl 3905  1pr 3911  ltaddpr 3934  chnle 5406  cvbr2t 5715  cvnbtwn2t 5719  cvnbtwn3t 5720  cvnbtwn4t 5721

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-ne 1192  df-pss 1494

metamath.org