Metamath Proof Explorer


Theorem frege55c

Description: Proposition 55 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege55c ( 𝑥 = 𝐴𝐴 = 𝑥 )

Proof

Step Hyp Ref Expression
1 vex 𝑥 ∈ V
2 1 frege54cor1c [ 𝑥 / 𝑦 ] 𝑦 = 𝑥
3 frege53c ( [ 𝑥 / 𝑦 ] 𝑦 = 𝑥 → ( 𝑥 = 𝐴[ 𝐴 / 𝑦 ] 𝑦 = 𝑥 ) )
4 2 3 ax-mp ( 𝑥 = 𝐴[ 𝐴 / 𝑦 ] 𝑦 = 𝑥 )
5 df-sbc ( [ 𝐴 / 𝑦 ] 𝑦 = 𝑥𝐴 ∈ { 𝑦𝑦 = 𝑥 } )
6 clelab ( 𝐴 ∈ { 𝑦𝑦 = 𝑥 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴𝑦 = 𝑥 ) )
7 5 6 bitri ( [ 𝐴 / 𝑦 ] 𝑦 = 𝑥 ↔ ∃ 𝑦 ( 𝑦 = 𝐴𝑦 = 𝑥 ) )
8 eqtr2 ( ( 𝑦 = 𝐴𝑦 = 𝑥 ) → 𝐴 = 𝑥 )
9 8 exlimiv ( ∃ 𝑦 ( 𝑦 = 𝐴𝑦 = 𝑥 ) → 𝐴 = 𝑥 )
10 7 9 sylbi ( [ 𝐴 / 𝑦 ] 𝑦 = 𝑥𝐴 = 𝑥 )
11 4 10 syl ( 𝑥 = 𝐴𝐴 = 𝑥 )