Theorem sbcid

Description: An identity theorem for substitution. See sbid . (Contributed by Mario Carneiro, 18-Feb-2017)

	Ref	Expression
Assertion	sbcid	$$⊢\underset{\dot{}}{[}x/x\underset{\dot{}}{]}\phi \leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		sbsbc	$$⊢\left[x/x\right]\phi \leftrightarrow \underset{\dot{}}{[}x/x\underset{\dot{}}{]}\phi$$
2		sbid	$$⊢\left[x/x\right]\phi \leftrightarrow \phi$$
3	1 2	bitr3i	$$⊢\underset{\dot{}}{[}x/x\underset{\dot{}}{]}\phi \leftrightarrow \phi$$