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 ] ph <-> [. y / x ]. ph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  y = y
2 dfsbcq2 
 |-  ( y = y -> ( [ y / x ] ph <-> [. y / x ]. ph ) )
3 1 2 ax-mp 
 |-  ( [ y / x ] ph <-> [. y / x ]. ph )