Theorem pssv

Description: Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998)

	Ref	Expression
Assertion	pssv	⊢ ( 𝐴 ⊊ V ↔ ¬ 𝐴 = V )

Proof

Step	Hyp	Ref	Expression
1		ssv	⊢ 𝐴 ⊆ V
2		dfpss2	⊢ ( 𝐴 ⊊ V ↔ ( 𝐴 ⊆ V ∧ ¬ 𝐴 = V ) )
3	1 2	mpbiran	⊢ ( 𝐴 ⊊ V ↔ ¬ 𝐴 = V )