Theorem sbsbc 3283

Description: Show that df-sb 1809 and df-sbc 3280 are equivalent when the class term A in df-sbc 3280 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1809 for proofs involving df-sbc 3280. (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 2462	. 2 |- y = y
2		dfsbcq2 3282	. 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 189   [wsb 1808   [.wsbc 3279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-clab 2449  df-cleq 2455  df-clel 2458  df-sbc 3280

This theorem is referenced by:  spsbc  3292  sbcid  3296  sbcco  3302  sbcco2  3303  sbcie2g  3313  eqsbc3  3319  sbcralt  3352  cbvralcsf  3407  cbvreucsf  3409  cbvrabcsf  3410  sbnfc2  3808  csbab  3809  wfis2fg  5436  isarep1  5684  tfindes  6716  tfinds2  6717  iuninc  28225  suppss2fOLD  28286  suppss2f  28287  fmptdF  28304  disjdsct  28332  esumpfinvalf  28946  measiuns  29088  bnj580  29773  bnj985  29813  setinds2f  30474  frins2fg  30534  bj-sbeq  31548  bj-sbel1  31552  bj-snsetex  31602  poimirlem25  32010  poimirlem26  32011  fdc1  32120  exlimddvfi  32407  frege52b  36530  frege58c  36562  pm13.194  36807  pm14.12  36816  sbiota1  36829  onfrALTlem1  36958  csbabgOLD  37251  onfrALTlem1VD  37327  disjinfi  37506  ellimcabssub0  37735