This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Subclasses and subsets ssnelpssd
Description: Subclass inclusion with one element of the superclass missing is proper
subclass inclusion. Deduction form of ssnelpss . (Contributed by David Moews , 1-May-2017)
Ref
Expression
Hypotheses
ssnelpssd.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
ssnelpssd.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
ssnelpssd.3 ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
Assertion
ssnelpssd ⊢ ( 𝜑 → 𝐴 ⊊ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
ssnelpssd.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2
ssnelpssd.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
3
ssnelpssd.3 ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
4
ssnelpss ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝐴 ⊊ 𝐵 ) )
5
1 4
syl ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝐴 ⊊ 𝐵 ) )
6
2 3 5
mp2and ⊢ ( 𝜑 → 𝐴 ⊊ 𝐵 )