Theorem sbsbc 3774

Description: Show that df-sb 2066 and df-sbc 3771 are equivalent when the class term 𝐴 in df-sbc 3771 is a setvar variable. This theorem lets us reuse theorems based on df-sb 2066 for proofs involving df-sbc 3771. (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 3773	. 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Syntax hints:   ↔ wb 206  [wsb 2065  [wsbc 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clab 2715  df-cleq 2728  df-clel 2810  df-sbc 3771

This theorem is referenced by:  spsbc  3783  sbcid  3787  sbccow  3793  sbcco  3796  sbcco2  3797  sbcie2g  3811  eqsbc1  3817  sbcralt  3852  cbvralcsf  3921  cbvreucsf  3923  cbvrabcsf  3924  sbnfc2  4419  csbab  4420  csbie2df  4423  2nreu  4424  frpoins2fg  6338  wfis2fgOLD  6351  isarep1OLD  6632  tfindes  7863  tfinds2  7864  frins2f  9772  iuninc  32546  suppss2f  32621  fmptdF  32639  disjdsct  32685  esumpfinvalf  34112  measiuns  34253  bnj580  34949  bnj985v  34989  bnj985  34990  xpab  35748  setinds2f  35802  bj-sbeq  36924  bj-sbel1  36928  bj-snsetex  36986  poimirlem25  37674  poimirlem26  37675  fdc1  37775  exlimddvfi  38151  frege52b  43880  frege58c  43912  pm13.194  44403  pm14.12  44412  sbiota1  44425  onfrALTlem1  44540  onfrALTlem1VD  44881  disjinfi  45183  ellimcabssub0  45613  2reu8i  47109  ich2exprop  47452  ichnreuop  47453  ichreuopeq  47454