Metamath Proof Explorer

Theorem dffrege115

Description: If from the circumstance that c is a result of an application of the procedure R to b , whatever b may be, it can be inferred that every result of an application of the procedure R to b is the same as c , then we say : "The procedure R is single-valued". Definition 115 of Frege1879 p. 77. (Contributed by RP, 7-Jul-2020)

Ref Expression
Assertion dffrege115 ⊢∀c∀bbRc→∀abRa→a=c↔Fun⁡R-1-1

Proof

Step Hyp Ref Expression
1 alcom ⊢∀c∀bbRc→∀abRa→a=c↔∀b∀cbRc→∀abRa→a=c
2 19.21v ⊢∀abRc→bRa→a=c↔bRc→∀abRa→a=c
3 impexp ⊢bRc∧bRa→a=c↔bRc→bRa→a=c
4 vex ⊢b∈V
5 vex ⊢c∈V
6 4 5 brcnv ⊢bR-1-1c↔cR-1b
7 df-br ⊢bR-1-1c↔bc∈R-1-1
8 5 4 brcnv ⊢cR-1b↔bRc
9 6 7 8 3bitr3ri ⊢bRc↔bc∈R-1-1
10 vex ⊢a∈V
11 4 10 brcnv ⊢bR-1-1a↔aR-1b
12 df-br ⊢bR-1-1a↔ba∈R-1-1
13 10 4 brcnv ⊢aR-1b↔bRa
14 11 12 13 3bitr3ri ⊢bRa↔ba∈R-1-1
15 9 14 anbi12ci ⊢bRc∧bRa↔ba∈R-1-1∧bc∈R-1-1
16 15 imbi1i ⊢bRc∧bRa→a=c↔ba∈R-1-1∧bc∈R-1-1→a=c
17 3 16 bitr3i ⊢bRc→bRa→a=c↔ba∈R-1-1∧bc∈R-1-1→a=c
18 17 albii ⊢∀abRc→bRa→a=c↔∀aba∈R-1-1∧bc∈R-1-1→a=c
19 2 18 bitr3i ⊢bRc→∀abRa→a=c↔∀aba∈R-1-1∧bc∈R-1-1→a=c
20 19 albii ⊢∀cbRc→∀abRa→a=c↔∀c∀aba∈R-1-1∧bc∈R-1-1→a=c
21 alcom ⊢∀c∀aba∈R-1-1∧bc∈R-1-1→a=c↔∀a∀cba∈R-1-1∧bc∈R-1-1→a=c
22 20 21 bitri ⊢∀cbRc→∀abRa→a=c↔∀a∀cba∈R-1-1∧bc∈R-1-1→a=c
23 opeq2 ⊢a=c→ba=bc
24 23 eleq1d ⊢a=c→ba∈R-1-1↔bc∈R-1-1
25 24 mo4 ⊢∃*aba∈R-1-1↔∀a∀cba∈R-1-1∧bc∈R-1-1→a=c
26 df-mo ⊢∃*aba∈R-1-1↔∃c∀aba∈R-1-1→a=c
27 22 25 26 3bitr2i ⊢∀cbRc→∀abRa→a=c↔∃c∀aba∈R-1-1→a=c
28 27 albii ⊢∀b∀cbRc→∀abRa→a=c↔∀b∃c∀aba∈R-1-1→a=c
29 relcnv ⊢Rel⁡R-1-1
30 29 biantrur ⊢∀b∃c∀aba∈R-1-1→a=c↔Rel⁡R-1-1∧∀b∃c∀aba∈R-1-1→a=c
31 dffun5 ⊢Fun⁡R-1-1↔Rel⁡R-1-1∧∀b∃c∀aba∈R-1-1→a=c
32 30 31 bitr4i ⊢∀b∃c∀aba∈R-1-1→a=c↔Fun⁡R-1-1
33 1 28 32 3bitri ⊢∀c∀bbRc→∀abRa→a=c↔Fun⁡R-1-1