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	⊢ ( ( 𝜑 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ) → ( 𝜑 → 𝐴 = 𝐵 ) )