Metamath Proof Explorer


Theorem frege79

Description: Distributed form of frege78 . Proposition 79 of Frege1879 p. 63. (Contributed by RP, 1-Jul-2020) (Revised by RP, 3-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege79.x 𝑋𝑈
frege79.y 𝑌𝑉
frege79.r 𝑅𝑊
frege79.a 𝐴𝐵
Assertion frege79 ( ( 𝑅 hereditary 𝐴 → ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝐴 ) ) → ( 𝑅 hereditary 𝐴 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌𝑌𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 frege79.x 𝑋𝑈
2 frege79.y 𝑌𝑉
3 frege79.r 𝑅𝑊
4 frege79.a 𝐴𝐵
5 1 2 3 4 frege78 ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝐴 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌𝑌𝐴 ) ) )
6 ax-frege2 ( ( 𝑅 hereditary 𝐴 → ( ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝐴 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌𝑌𝐴 ) ) ) → ( ( 𝑅 hereditary 𝐴 → ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝐴 ) ) → ( 𝑅 hereditary 𝐴 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌𝑌𝐴 ) ) ) )
7 5 6 ax-mp ( ( 𝑅 hereditary 𝐴 → ∀ 𝑎 ( 𝑋 𝑅 𝑎𝑎𝐴 ) ) → ( 𝑅 hereditary 𝐴 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌𝑌𝐴 ) ) )