Theorem frege55lem2c 41202

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

Assertion

Ref	Expression
frege55lem2c	⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥)

Distinct variable group:   𝑥,𝑧

Allowed substitution hints:   𝐴(𝑥,𝑧)

Proof of Theorem frege55lem2c

Step	Hyp	Ref	Expression
1		vex 3412	. . 3 ⊢ 𝑥 ∈ V
2	1	frege54cor1c 41200	. 2 ⊢ [𝑥 / 𝑧]𝑧 = 𝑥
3		frege53c 41199	. 2 ⊢ ([𝑥 / 𝑧]𝑧 = 𝑥 → (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥))
4	2, 3	ax-mp 5	1 ⊢ (𝑥 = 𝐴 → [𝐴 / 𝑧]𝑧 = 𝑥)

Syntax hints:   → wi 4   = wceq 1543  Vcvv 3408  [wsbc 3694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-frege8 41094  ax-frege52c 41173

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-sbc 3695  df-sn 4542

This theorem is referenced by: (None)