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 y x φ [˙y / x]˙ φ


Step Hyp Ref Expression
1 eqid y = y
2 dfsbcq2 y = y y x φ [˙y / x]˙ φ
3 1 2 ax-mp y x φ [˙y / x]˙ φ