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

Proof

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