Description: A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002)
Ref | Expression | ||
---|---|---|---|
Assertion | ssnelpss | ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝐴 ⊊ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nelneq2 | ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴 ) → ¬ 𝐵 = 𝐴 ) | |
2 | eqcom | ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 ) | |
3 | 1 2 | sylnib | ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴 ) → ¬ 𝐴 = 𝐵 ) |
4 | dfpss2 | ⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵 ) ) | |
5 | 4 | baibr | ⊢ ( 𝐴 ⊆ 𝐵 → ( ¬ 𝐴 = 𝐵 ↔ 𝐴 ⊊ 𝐵 ) ) |
6 | 3 5 | syl5ib | ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝐴 ⊊ 𝐵 ) ) |