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 ) ) ) ) |