Metamath Proof Explorer

Theorem frege116

Description: One direction of dffrege115 . Proposition 116 of Frege1879 p. 77. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege116.x ⊢X∈U
Assertion frege116 ⊢Fun⁡R-1-1→∀bbRX→∀abRa→a=X

Proof

Step Hyp Ref Expression
1 frege116.x ⊢X∈U
2 dffrege115 ⊢∀c∀bbRc→∀abRa→a=c↔Fun⁡R-1-1
3 1 frege68c ⊢∀c∀bbRc→∀abRa→a=c↔Fun⁡R-1-1→Fun⁡R-1-1→[˙X/c]˙∀bbRc→∀abRa→a=c
4 sbcal ⊢[˙X/c]˙∀bbRc→∀abRa→a=c↔∀b[˙X/c]˙bRc→∀abRa→a=c
5 sbcimg ⊢X∈U→[˙X/c]˙bRc→∀abRa→a=c↔[˙X/c]˙bRc→[˙X/c]˙∀abRa→a=c
6 1 5 ax-mp ⊢[˙X/c]˙bRc→∀abRa→a=c↔[˙X/c]˙bRc→[˙X/c]˙∀abRa→a=c
7 sbcbr2g ⊢X∈U→[˙X/c]˙bRc↔bR⦋X/c⦌c
8 1 7 ax-mp ⊢[˙X/c]˙bRc↔bR⦋X/c⦌c
9 csbvarg ⊢X∈U→⦋X/c⦌c=X
10 1 9 ax-mp ⊢⦋X/c⦌c=X
11 10 breq2i ⊢bR⦋X/c⦌c↔bRX
12 8 11 bitri ⊢[˙X/c]˙bRc↔bRX
13 sbcal ⊢[˙X/c]˙∀abRa→a=c↔∀a[˙X/c]˙bRa→a=c
14 sbcimg ⊢X∈U→[˙X/c]˙bRa→a=c↔[˙X/c]˙bRa→[˙X/c]˙a=c
15 1 14 ax-mp ⊢[˙X/c]˙bRa→a=c↔[˙X/c]˙bRa→[˙X/c]˙a=c
16 sbcg ⊢X∈U→[˙X/c]˙bRa↔bRa
17 1 16 ax-mp ⊢[˙X/c]˙bRa↔bRa
18 sbceq2g ⊢X∈U→[˙X/c]˙a=c↔a=⦋X/c⦌c
19 1 18 ax-mp ⊢[˙X/c]˙a=c↔a=⦋X/c⦌c
20 10 eqeq2i ⊢a=⦋X/c⦌c↔a=X
21 19 20 bitri ⊢[˙X/c]˙a=c↔a=X
22 17 21 imbi12i ⊢[˙X/c]˙bRa→[˙X/c]˙a=c↔bRa→a=X
23 15 22 bitri ⊢[˙X/c]˙bRa→a=c↔bRa→a=X
24 23 albii ⊢∀a[˙X/c]˙bRa→a=c↔∀abRa→a=X
25 13 24 bitri ⊢[˙X/c]˙∀abRa→a=c↔∀abRa→a=X
26 12 25 imbi12i ⊢[˙X/c]˙bRc→[˙X/c]˙∀abRa→a=c↔bRX→∀abRa→a=X
27 6 26 bitri ⊢[˙X/c]˙bRc→∀abRa→a=c↔bRX→∀abRa→a=X
28 27 albii ⊢∀b[˙X/c]˙bRc→∀abRa→a=c↔∀bbRX→∀abRa→a=X
29 4 28 bitri ⊢[˙X/c]˙∀bbRc→∀abRa→a=c↔∀bbRX→∀abRa→a=X
30 3 29 imbitrdi ⊢∀c∀bbRc→∀abRa→a=c↔Fun⁡R-1-1→Fun⁡R-1-1→∀bbRX→∀abRa→a=X
31 2 30 ax-mp ⊢Fun⁡R-1-1→∀bbRX→∀abRa→a=X