Theorem dfpss2

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996)

	Ref	Expression
Assertion	dfpss2	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-pss	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
2		df-ne	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
3	2	anbi2i	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) )
4	1 3	bitri	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) )