Theorem sbsbc

Description: Show that df-sb and df-sbc are equivalent when the class term A in df-sbc is a setvar variable. This theorem lets us reuse theorems based on df-sb for proofs involving df-sbc . (Contributed by NM, 31-Dec-2016) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢y=y$$
2		dfsbcq2	$$⊢y=y\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
3	1 2	ax-mp	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$