axnul-with-subst Show Code edit
# Here is a corollary which we'll use shortly.
thm (axnul-with-subst () () (∃ emptySet (∀ y (↔ (∈ y emptySet) (subst y z (⊥)))))
emptySet y axnul
(∃ emptySet (∀ y (¬ (∈ y emptySet))))
# We start with ¬ y ∈ emptySet ↔ (y ∈ emptySet ↔ [ y / z ] ⊥)
(∈ y emptySet) NegationBiconditional
(↔ (¬ (∈ y emptySet)) (↔ (∈ y emptySet) (⊥)))
y z (⊥) NullSubstitution
(↔ (subst y z (⊥)) (⊥))
swapBiconditional
(↔ (⊥) (subst y z (⊥)))
(∈ y emptySet) buildBiconditionalLL
(↔ (↔ (∈ y emptySet) (⊥)) (↔ (∈ y emptySet) (subst y z (⊥))))
applyBiconditionalTransitivity
(↔ (¬ (∈ y emptySet)) (↔ (∈ y emptySet) (subst y z (⊥))))
# Combining that with axnul we are done.
eliminateBiconditionalReverse
(→ (¬ (∈ y emptySet)) (↔ (∈ y emptySet) (subst y z (⊥))))
y addForAll
(→ (∀ y (¬ (∈ y emptySet))) (∀ y (↔ (∈ y emptySet) (subst y z (⊥)))))
emptySet addThereExists
(→ (∃ emptySet (∀ y (¬ (∈ y emptySet)))) (∃ emptySet (∀ y (↔ (∈ y emptySet) (subst y z (⊥))))))
applyModusPonens
(∃ emptySet (∀ y (↔ (∈ y emptySet) (subst y z (⊥)))))
)
edit