Metamath Proof Explorer


Theorem frege55lem1c

Description: Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion frege55lem1c ( ( 𝜑[ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ) → ( 𝜑𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-sbc ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐵𝐴 ∈ { 𝑥𝑥 = 𝐵 } )
2 eqeq1 ( 𝑥 = 𝐴 → ( 𝑥 = 𝐵𝐴 = 𝐵 ) )
3 2 elabg ( 𝐴 ∈ { 𝑥𝑥 = 𝐵 } → ( 𝐴 ∈ { 𝑥𝑥 = 𝐵 } ↔ 𝐴 = 𝐵 ) )
4 3 ibi ( 𝐴 ∈ { 𝑥𝑥 = 𝐵 } → 𝐴 = 𝐵 )
5 1 4 sylbi ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐵𝐴 = 𝐵 )
6 5 imim2i ( ( 𝜑[ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ) → ( 𝜑𝐴 = 𝐵 ) )