Theorem sbsbc 3757

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 209  [wsb 2097  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3754

This theorem is referenced by:  spsbc  3766  sbcid  3770  sbccow  3776  sbcco  3779  sbcco2  3780  sbcie2g  3793  eqsbc1  3799  sbcralt  3834  cbvralcsf  3903  cbvreucsf  3905  cbvrabcsf  3906  sbnfc2  4410  csbab  4411  csbie2df  4414  2nreu  4415  frpoins2fg  6346  tfindes  7859  tfinds2  7860  setinds2f  9719  frins2f  9725  iuninc  32846  suppss2f  32924  fmptdF  32942  disjdsct  32989  esumpfinvalf  34411  measiuns  34552  bnj580  35246  bnj985v  35286  bnj985  35287  xpab  36151  bj-df-sb  37195  bj-sbeq  37459  bj-sbel1  37463  bj-snsetex  37521  poimirlem25  38218  poimirlem26  38219  fdc1  38319  exlimddvfi  38695  frege52b  44541  frege58c  44573  pm13.194  45048  pm14.12  45057  sbiota1  45070  onfrALTlem1  45183  onfrALTlem1VD  45524  disjinfi  45836  ellimcabssub0  46259  2reu8i  47773  ich2exprop  48143  ichnreuop  48144  ichreuopeq  48145