Metamath Proof Explorer


Theorem frege74

Description: If X has a property A that is hereditary in the R -sequence, then every result of a application of the procedure R to X has the property A . Proposition 74 of Frege1879 p. 60. (Contributed by RP, 28-Mar-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

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

Proof

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