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 𝑋𝑈
frege74.y 𝑌𝑉
Assertion frege74 ( 𝑋𝐴 → ( 𝑅 hereditary 𝐴 → ( 𝑋 𝑅 𝑌𝑌𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 frege74.x 𝑋𝑈
2 frege74.y 𝑌𝑉
3 1 2 frege72 ( 𝑅 hereditary 𝐴 → ( 𝑋𝐴 → ( 𝑋 𝑅 𝑌𝑌𝐴 ) ) )
4 ax-frege8 ( ( 𝑅 hereditary 𝐴 → ( 𝑋𝐴 → ( 𝑋 𝑅 𝑌𝑌𝐴 ) ) ) → ( 𝑋𝐴 → ( 𝑅 hereditary 𝐴 → ( 𝑋 𝑅 𝑌𝑌𝐴 ) ) ) )
5 3 4 ax-mp ( 𝑋𝐴 → ( 𝑅 hereditary 𝐴 → ( 𝑋 𝑅 𝑌𝑌𝐴 ) ) )