This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 𝑦 = 𝑦
2		dfsbcq2	⊢ ( 𝑦 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
3	1 2	ax-mp	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )