# Metamath Proof Explorer

## Theorem frege118

Description: Simplified application of one direction of dffrege115 . Proposition 118 of Frege1879 p. 78. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege116.x ${⊢}{X}\in {U}$
frege118.y ${⊢}{Y}\in {V}$
Assertion frege118 ${⊢}\mathrm{Fun}{{{R}}^{-1}}^{-1}\to \left({Y}{R}{X}\to \forall {a}\phantom{\rule{.4em}{0ex}}\left({Y}{R}{a}\to {a}={X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 frege116.x ${⊢}{X}\in {U}$
2 frege118.y ${⊢}{Y}\in {V}$
3 2 frege58c
4 sbcimg
5 2 4 ax-mp
6 sbcbr1g
7 2 6 ax-mp
8 csbvarg
9 2 8 ax-mp
10 9 breq1i
11 7 10 bitri
12 sbcal
13 sbcimg
14 2 13 ax-mp
15 sbcbr1g
16 2 15 ax-mp
17 9 breq1i
18 16 17 bitri
19 sbcg
20 2 19 ax-mp
21 18 20 imbi12i
22 14 21 bitri
23 22 albii
24 12 23 bitri
25 11 24 imbi12i
26 5 25 bitri
27 3 26 sylib ${⊢}\forall {b}\phantom{\rule{.4em}{0ex}}\left({b}{R}{X}\to \forall {a}\phantom{\rule{.4em}{0ex}}\left({b}{R}{a}\to {a}={X}\right)\right)\to \left({Y}{R}{X}\to \forall {a}\phantom{\rule{.4em}{0ex}}\left({Y}{R}{a}\to {a}={X}\right)\right)$
28 1 frege117 ${⊢}\left(\forall {b}\phantom{\rule{.4em}{0ex}}\left({b}{R}{X}\to \forall {a}\phantom{\rule{.4em}{0ex}}\left({b}{R}{a}\to {a}={X}\right)\right)\to \left({Y}{R}{X}\to \forall {a}\phantom{\rule{.4em}{0ex}}\left({Y}{R}{a}\to {a}={X}\right)\right)\right)\to \left(\mathrm{Fun}{{{R}}^{-1}}^{-1}\to \left({Y}{R}{X}\to \forall {a}\phantom{\rule{.4em}{0ex}}\left({Y}{R}{a}\to {a}={X}\right)\right)\right)$
29 27 28 ax-mp ${⊢}\mathrm{Fun}{{{R}}^{-1}}^{-1}\to \left({Y}{R}{X}\to \forall {a}\phantom{\rule{.4em}{0ex}}\left({Y}{R}{a}\to {a}={X}\right)\right)$