Metamath Proof Explorer


Theorem frege117

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

Ref Expression
Hypothesis frege116.x 𝑋𝑈
Assertion frege117 ( ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 frege116.x 𝑋𝑈
2 1 frege116 ( Fun 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) )
3 frege9 ( ( Fun 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) ) → ( ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) ) ) )
4 2 3 ax-mp ( ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑎 = 𝑋 ) ) ) )