EmptySet Show Code edit
thm (EmptySet () () (¬ (∈ A (∅)))
# The substitution to apply <code>VariableToObject</code> is <code>x = A → x ∉ ∅ ↔ A ∉ ∅</code>
x A (∅) MembershipBuilderRR
(→ (= x A) (↔ (∈ x (∅)) (∈ A (∅))))
addNegationInConsequent
(→ (= x A) (↔ (¬ (∈ x (∅))) (¬ (∈ A (∅)))))
x EmptySetVariable
(¬ (∈ x (∅)))
VariableToObject
(¬ (∈ A (∅)))
)
edit