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 ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴 → 𝐴 = 𝑋 ) ) ) ) |
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 ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴 → 𝐴 = 𝑋 ) ) ) ) |