Metamath Proof Explorer


Theorem frege73

Description: Lemma for frege87 . Proposition 73 of Frege1879 p. 59. (Contributed by RP, 28-Mar-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege73.x
|- X e. U
frege73.y
|- Y e. V
Assertion frege73
|- ( ( R hereditary A -> X e. A ) -> ( R hereditary A -> ( X R Y -> Y e. A ) ) )

Proof

Step Hyp Ref Expression
1 frege73.x
 |-  X e. U
2 frege73.y
 |-  Y e. V
3 1 2 frege72
 |-  ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) )
4 ax-frege2
 |-  ( ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) ) -> ( ( R hereditary A -> X e. A ) -> ( R hereditary A -> ( X R Y -> Y e. A ) ) ) )
5 3 4 ax-mp
 |-  ( ( R hereditary A -> X e. A ) -> ( R hereditary A -> ( X R Y -> Y e. A ) ) )