Theorem sbsbc 3795

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 206  [wsb 2062  [wsbc 3791

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792

This theorem is referenced by:  spsbc  3804  sbcid  3808  sbccow  3814  sbcco  3817  sbcco2  3818  sbcie2g  3834  eqsbc1  3841  sbcralt  3881  cbvralcsf  3953  cbvreucsf  3955  cbvrabcsf  3956  sbnfc2  4445  csbab  4446  csbie2df  4449  2nreu  4450  frpoins2fg  6367  wfis2fgOLD  6380  isarep1OLD  6658  tfindes  7884  tfinds2  7885  frins2f  9791  iuninc  32581  suppss2f  32655  fmptdF  32673  disjdsct  32718  esumpfinvalf  34057  measiuns  34198  bnj580  34906  bnj985v  34946  bnj985  34947  xpab  35706  setinds2f  35761  bj-sbeq  36884  bj-sbel1  36888  bj-snsetex  36946  poimirlem25  37632  poimirlem26  37633  fdc1  37733  exlimddvfi  38109  frege52b  43879  frege58c  43911  pm13.194  44408  pm14.12  44417  sbiota1  44430  onfrALTlem1  44546  onfrALTlem1VD  44888  disjinfi  45135  ellimcabssub0  45573  2reu8i  47063  ich2exprop  47396  ichnreuop  47397  ichreuopeq  47398