This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes) Define proper substitution sbequ
Description: Equality property for substitution, from Tarski's system. Used in proof
of Theorem 9.7 in Megill p. 449 (p. 16 of the preprint). (Contributed by NM , 14-May-1993) Revise df-sb . (Revised by BJ , 30-Dec-2020)
Ref
Expression
Assertion
sbequ ⊢ x = y → x z φ ↔ y z φ
Proof
Step
Hyp
Ref
Expression
1
equequ2 ⊢ x = y → u = x ↔ u = y
2
1
imbi1d ⊢ x = y → u = x → ∀ z z = u → φ ↔ u = y → ∀ z z = u → φ
3
2
albidv ⊢ x = y → ∀ u u = x → ∀ z z = u → φ ↔ ∀ u u = y → ∀ z z = u → φ
4
dfsb ⊢ x z φ ↔ ∀ u u = x → ∀ z z = u → φ
5
dfsb ⊢ y z φ ↔ ∀ u u = y → ∀ z z = u → φ
6
3 4 5
3bitr4g ⊢ x = y → x z φ ↔ y z φ