Theorem sbsbc 3303

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

Assertion

Ref	Expression
sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )

Proof of Theorem sbsbc

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

Syntax hints:   <-> wb 187   [wsb 1786   [.wsbc 3299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-clab 2408  df-cleq 2414  df-clel 2417  df-sbc 3300

This theorem is referenced by:  spsbc  3312  sbcid  3316  sbcco  3322  sbcco2  3323  sbcie2g  3333  eqsbc3  3339  sbcralt  3372  cbvralcsf  3427  cbvreucsf  3429  cbvrabcsf  3430  sbnfc2  3824  csbab  3825  wfis2fg  5432  isarep1  5676  tfindes  6699  tfinds2  6700  iuninc  28165  suppss2fOLD  28226  suppss2f  28227  fmptdF  28244  disjdsct  28272  esumpfinvalf  28892  measiuns  29034  bnj580  29719  bnj985  29759  setinds2f  30419  frins2fg  30479  bj-sbeq  31459  bj-sbel1  31463  bj-snsetex  31512  poimirlem25  31878  poimirlem26  31879  fdc1  31988  exlimddvfi  32275  frege52b  36342  frege58c  36374  pm13.194  36620  pm14.12  36629  sbiota1  36642  onfrALTlem1  36771  csbabgOLD  37071  onfrALTlem1VD  37147  disjinfi  37317  ellimcabssub0  37516