Theorem sbsbc 3775

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 208  [wsb 2065  [wsbc 3771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772

This theorem is referenced by:  spsbc  3784  sbcid  3788  sbccow  3794  sbcco  3797  sbcco2  3798  sbcie2g  3810  eqsbc3  3816  eqsbc3OLD  3817  sbcralt  3854  cbvralcsf  3924  cbvreucsf  3926  cbvrabcsf  3927  sbnfc2  4387  csbab  4388  csbie2df  4391  2nreu  4392  wfis2fg  6179  isarep1  6436  tfindes  7571  tfinds2  7572  iuninc  30306  suppss2f  30378  fmptdF  30395  disjdsct  30432  esumpfinvalf  31330  measiuns  31471  bnj580  32180  bnj985v  32220  bnj985  32221  setinds2f  33019  frpoins2fg  33077  frins2fg  33084  bj-sbeq  34213  bj-sbel1  34217  bj-snsetex  34270  poimirlem25  34911  poimirlem26  34912  fdc1  35015  exlimddvfi  35394  frege52b  40228  frege58c  40260  pm13.194  40737  pm14.12  40746  sbiota1  40759  onfrALTlem1  40875  onfrALTlem1VD  41217  disjinfi  41447  ellimcabssub0  41891  2reu8i  43306  ich2exprop  43627  ichnreuop  43628  ichreuopeq  43629