Description: Lemma for frege72 . Proposition 71 of Frege1879 p. 59. (Contributed by RP, 28-Mar-2020) (Revised by RP, 3-Jul-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | frege71.x | |- X e. V |
|
Assertion | frege71 | |- ( ( A. z ( X R z -> z e. A ) -> ( X R Y -> Y e. A ) ) -> ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege71.x | |- X e. V |
|
2 | 1 | frege70 | |- ( R hereditary A -> ( X e. A -> A. z ( X R z -> z e. A ) ) ) |
3 | frege19 | |- ( ( R hereditary A -> ( X e. A -> A. z ( X R z -> z e. A ) ) ) -> ( ( A. z ( X R z -> z e. A ) -> ( X R Y -> Y e. A ) ) -> ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) ) ) ) |
|
4 | 2 3 | ax-mp | |- ( ( A. z ( X R z -> z e. A ) -> ( X R Y -> Y e. A ) ) -> ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) ) ) |