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	⊢ ( ¬ 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 → 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		pm4.61	⊢ ( ¬ ( 𝐴 ⊆ 𝐵 → 𝐴 = 𝐵 ) ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
2		dfpss2	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
3	1 2	bitr4i	⊢ ( ¬ ( 𝐴 ⊆ 𝐵 → 𝐴 = 𝐵 ) ↔ 𝐴 ⊊ 𝐵 )
4	3	con1bii	⊢ ( ¬ 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 → 𝐴 = 𝐵 ) )