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 Define basic set operations and relations eldifd
Description: If a class is in one class and not another, it is also in their
difference. One-way deduction form of eldif . (Contributed by David
Moews , 1-May-2017)
Ref
Expression
Hypotheses
eldifd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
eldifd.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐶 )
Assertion
eldifd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) )
Proof
Step
Hyp
Ref
Expression
1
eldifd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2
eldifd.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐶 )
3
eldif ⊢ ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) )
4
1 2 3
sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) )