Theorem sbsbc 3791

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2063  [wsbc 3787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clab 2714  df-cleq 2728  df-clel 2815  df-sbc 3788

This theorem is referenced by:  spsbc  3800  sbcid  3804  sbccow  3810  sbcco  3813  sbcco2  3814  sbcie2g  3828  eqsbc1  3834  sbcralt  3871  cbvralcsf  3940  cbvreucsf  3942  cbvrabcsf  3943  sbnfc2  4438  csbab  4439  csbie2df  4442  2nreu  4443  frpoins2fg  6364  wfis2fgOLD  6377  isarep1OLD  6656  tfindes  7885  tfinds2  7886  frins2f  9794  iuninc  32574  suppss2f  32649  fmptdF  32667  disjdsct  32713  esumpfinvalf  34078  measiuns  34219  bnj580  34928  bnj985v  34968  bnj985  34969  xpab  35727  setinds2f  35781  bj-sbeq  36903  bj-sbel1  36907  bj-snsetex  36965  poimirlem25  37653  poimirlem26  37654  fdc1  37754  exlimddvfi  38130  frege52b  43907  frege58c  43939  pm13.194  44436  pm14.12  44445  sbiota1  44458  onfrALTlem1  44573  onfrALTlem1VD  44915  disjinfi  45202  ellimcabssub0  45637  2reu8i  47130  ich2exprop  47463  ichnreuop  47464  ichreuopeq  47465