SetObject Show Code edit
thm (SetObject
((C y) (φz y result) (φy z) (φC y))
(HSUBZ (→ (= z y) (↔ φz φy)) HSUBC (→ (= y C) (↔ φy φC)) HEXISTS (∃ result (∀ y (↔ (∈ y result) φy))))
(↔ (∈ C (abstract z φz)) φC)
# Our substitution is <code>y = C → ((y ∈ {z | φz} ↔ φy) ↔ (C ∈ {z | φz} ↔ φC))</code>.
y C (abstract z φz) MembershipBuilderRR
(→ (= y C) (↔ (∈ y (abstract z φz)) (∈ C (abstract z φz))))
HSUBC
(→ (= y C) (↔ φy φC))
buildBiconditionalInConsequent
(→ (= y C) (↔ (↔ (∈ y (abstract z φz)) φy) (↔ (∈ C (abstract z φz)) φC)))
HSUBZ
(→ (= z y) (↔ φz φy))
HEXISTS
(∃ result (∀ y (↔ (∈ y result) φy)))
SetVariable
(↔ (∈ y (abstract z φz)) φy)
VariableToObject
(↔ (∈ C (abstract z φz)) φC)
)
edit