Metamath Proof Explorer


Theorem frege119

Description: Lemma for frege120 . Proposition 119 of Frege1879 p. 78. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege116.x 𝑋𝑈
frege118.y 𝑌𝑉
Assertion frege119 ( ( ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) → ( 𝑌 𝑅 𝐴𝐴 = 𝑋 ) ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴𝐴 = 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 frege116.x 𝑋𝑈
2 frege118.y 𝑌𝑉
3 1 2 frege118 ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) )
4 frege19 ( ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) ) → ( ( ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) → ( 𝑌 𝑅 𝐴𝐴 = 𝑋 ) ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴𝐴 = 𝑋 ) ) ) ) )
5 3 4 ax-mp ( ( ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) → ( 𝑌 𝑅 𝐴𝐴 = 𝑋 ) ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴𝐴 = 𝑋 ) ) ) )