Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Following in a sequence
frege82
Metamath Proof Explorer
Description: Closed-form deduction based on frege81 . Proposition 82 of
Frege1879 p. 64. (Contributed by RP , 1-Jul-2020) (Revised by RP , 5-Jul-2020) (Proof modification is discouraged.)
Ref
Expression
Hypotheses
frege82.x
⊢ X ∈ U
frege82.y
⊢ Y ∈ V
frege82.r
⊢ R ∈ W
frege82.a
⊢ A ∈ B
Assertion
frege82
⊢ φ → X ∈ A → R hereditary A → φ → X t+ ⁡ R Y → Y ∈ A
Proof
Step
Hyp
Ref
Expression
1
frege82.x
⊢ X ∈ U
2
frege82.y
⊢ Y ∈ V
3
frege82.r
⊢ R ∈ W
4
frege82.a
⊢ A ∈ B
5
1 2 3 4
frege81
⊢ X ∈ A → R hereditary A → X t+ ⁡ R Y → Y ∈ A
6
frege18
⊢ X ∈ A → R hereditary A → X t+ ⁡ R Y → Y ∈ A → φ → X ∈ A → R hereditary A → φ → X t+ ⁡ R Y → Y ∈ A
7
5 6
ax-mp
⊢ φ → X ∈ A → R hereditary A → φ → X t+ ⁡ R Y → Y ∈ A