Theorem sbid2

Description: An identity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 . Check out sbid2vw for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 6-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbid2.1	$$⊢Ⅎx\phi$$
Assertion	sbid2	$$⊢\left[y/x\right]\left[x/y\right]\phi \leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		sbid2.1	$$⊢Ⅎx\phi$$
2		sbco	$$⊢\left[y/x\right]\left[x/y\right]\phi \leftrightarrow \left[y/x\right]\phi$$
3	1	sbf	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$
4	2 3	bitri	$$⊢\left[y/x\right]\left[x/y\right]\phi \leftrightarrow \phi$$