Theorem sbsbc 3340

Description: Show that df-sb 1712 and df-sbc 3337 are equivalent when the class term A in df-sbc 3337 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1712 for proofs involving df-sbc 3337. (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 2467	. 2 |- y = y
2		dfsbcq2 3339	. 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 184   [wsb 1711   [.wsbc 3336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-clab 2453  df-cleq 2459  df-clel 2462  df-sbc 3337

This theorem is referenced by:  spsbc  3349  sbcid  3353  sbcco  3359  sbcco2  3360  sbcie2g  3370  eqsbc3  3376  sbcralt  3417  cbvralcsf  3472  cbvreucsf  3474  cbvrabcsf  3475  sbnfc2  3859  csbab  3860  csbabgOLD  3861  isarep1  5673  tfindes  6692  tfinds2  6693  iuninc  27251  suppss2f  27300  fmptdF  27318  disjdsct  27344  esumpfinvalf  27907  measiuns  28013  setinds2f  29138  wfis2fg  29218  frins2fg  29254  fdc1  30166  exlimddvfi  30454  pm13.194  31221  pm14.12  31230  sbiota1  31243  ellimcabssub0  31482  onfrALTlem1  32801  onfrALTlem1VD  33171  bnj580  33451  bnj985  33491  bj-sbeq  33950  bj-sbel1  33954  bj-snsetex  34003