Metamath Proof Explorer


Theorem frege71

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

Proof

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