Theorem npss

Description: A class is not a proper subclass of another iff it satisfies a one-directional form of eqss . (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	npss	|- ( -. A C. B <-> ( A C_ B -> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		pm4.61	|- ( -. ( A C_ B -> A = B ) <-> ( A C_ B /\ -. A = B ) )
2		dfpss2	|- ( A C. B <-> ( A C_ B /\ -. A = B ) )
3	1 2	bitr4i	|- ( -. ( A C_ B -> A = B ) <-> A C. B )
4	3	con1bii	|- ( -. A C. B <-> ( A C_ B -> A = B ) )