Theorem sbsbc 3331

Description: Show that df-sb 1741 and df-sbc 3328 are equivalent when the class term A in df-sbc 3328 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1741 for proofs involving df-sbc 3328. (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 2457	. 2 |- y = y
2		dfsbcq2 3330	. 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 1740   [.wsbc 3327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328

This theorem is referenced by:  spsbc  3340  sbcid  3344  sbcco  3350  sbcco2  3351  sbcie2g  3361  eqsbc3  3367  sbcralt  3406  cbvralcsf  3462  cbvreucsf  3464  cbvrabcsf  3465  sbnfc2  3859  csbab  3860  csbabgOLD  3861  isarep1  5673  tfindes  6696  tfinds2  6697  iuninc  27567  suppss2f  27625  fmptdF  27643  disjdsct  27676  esumpfinvalf  28248  measiuns  28361  setinds2f  29407  wfis2fg  29487  frins2fg  29523  fdc1  30423  exlimddvfi  30711  pm13.194  31502  pm14.12  31511  sbiota1  31524  ellimcabssub0  31805  onfrALTlem1  33442  onfrALTlem1VD  33812  bnj580  34093  bnj985  34133  bj-sbeq  34590  bj-sbel1  34594  bj-snsetex  34643  frege52b  38038  frege58c  38070  frege72  38085