# Metamath Proof Explorer

## Theorem frege120

Description: Simplified application of one direction of dffrege115 . Proposition 120 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}$
frege120.a ${⊢}{A}\in {W}$
Assertion frege120 ${⊢}\mathrm{Fun}{{{R}}^{-1}}^{-1}\to \left({Y}{R}{X}\to \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 frege120.a ${⊢}{A}\in {W}$
4 3 frege58c
5 sbcim1
6 sbcbr2g
7 3 6 ax-mp
8 csbvarg
9 3 8 ax-mp
10 9 breq2i
11 7 10 bitri
12 sbceq1g
13 3 12 ax-mp
14 9 eqeq1i
15 13 14 bitri
16 5 11 15 3imtr3g
17 4 16 syl ${⊢}\forall {a}\phantom{\rule{.4em}{0ex}}\left({Y}{R}{a}\to {a}={X}\right)\to \left({Y}{R}{A}\to {A}={X}\right)$
18 1 2 frege119 ${⊢}\left(\forall {a}\phantom{\rule{.4em}{0ex}}\left({Y}{R}{a}\to {a}={X}\right)\to \left({Y}{R}{A}\to {A}={X}\right)\right)\to \left(\mathrm{Fun}{{{R}}^{-1}}^{-1}\to \left({Y}{R}{X}\to \left({Y}{R}{A}\to {A}={X}\right)\right)\right)$
19 17 18 ax-mp ${⊢}\mathrm{Fun}{{{R}}^{-1}}^{-1}\to \left({Y}{R}{X}\to \left({Y}{R}{A}\to {A}={X}\right)\right)$