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	⊢ ( 𝑥 = 𝐴 → 𝐴 = 𝑥 )