Theorem sbsbc 3742

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2067  [wsbc 3738

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clab 2713  df-cleq 2726  df-clel 2809  df-sbc 3739

This theorem is referenced by:  spsbc  3751  sbcid  3755  sbccow  3761  sbcco  3764  sbcco2  3765  sbcie2g  3779  eqsbc1  3785  sbcralt  3820  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  sbnfc2  4389  csbab  4390  csbie2df  4393  2nreu  4394  frpoins2fg  6300  tfindes  7803  tfinds2  7804  setinds2f  9657  frins2f  9663  iuninc  32584  suppss2f  32665  fmptdF  32683  disjdsct  32731  esumpfinvalf  34182  measiuns  34323  bnj580  35018  bnj985v  35058  bnj985  35059  xpab  35869  bj-df-sb  36796  bj-sbeq  37045  bj-sbel1  37049  bj-snsetex  37107  poimirlem25  37785  poimirlem26  37786  fdc1  37886  exlimddvfi  38262  frege52b  44072  frege58c  44104  pm13.194  44595  pm14.12  44604  sbiota1  44617  onfrALTlem1  44731  onfrALTlem1VD  45072  disjinfi  45378  ellimcabssub0  45805  2reu8i  47301  ich2exprop  47659  ichnreuop  47660  ichreuopeq  47661