Theorem sbsbc 3781

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

Assertion

Ref	Expression
sbsbc	⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Proof of Theorem sbsbc

Step	Hyp	Ref	Expression
1		eqid 2731	. 2 ⊢ 𝑦 = 𝑦
2		dfsbcq2 3780	. 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Syntax hints:   ↔ wb 205  [wsb 2066  [wsbc 3777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-clab 2709  df-cleq 2723  df-clel 2809  df-sbc 3778

This theorem is referenced by:  spsbc  3790  sbcid  3794  sbccow  3800  sbcco  3803  sbcco2  3804  sbcie2g  3819  eqsbc1  3826  sbcralt  3866  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  sbnfc2  4436  csbab  4437  csbie2df  4440  2nreu  4441  frpoins2fg  6345  wfis2fgOLD  6358  isarep1OLD  6638  tfindes  7856  tfinds2  7857  frins2f  9754  iuninc  32225  suppss2f  32296  fmptdF  32314  disjdsct  32357  esumpfinvalf  33538  measiuns  33679  bnj580  34388  bnj985v  34428  bnj985  34429  xpab  35165  setinds2f  35221  bj-sbeq  36245  bj-sbel1  36249  bj-snsetex  36308  poimirlem25  36977  poimirlem26  36978  fdc1  37078  exlimddvfi  37454  frege52b  43103  frege58c  43135  pm13.194  43634  pm14.12  43643  sbiota1  43656  onfrALTlem1  43772  onfrALTlem1VD  44114  disjinfi  44350  ellimcabssub0  44792  2reu8i  46280  ich2exprop  46598  ichnreuop  46599  ichreuopeq  46600