Theorem sbsbc 3757

Description: Show that df-sb 2066 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 2066 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 2729	. 2 ⊢ 𝑦 = 𝑦
2		dfsbcq2 3756	. 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	ax-mp 5	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754

This theorem is referenced by:  spsbc  3766  sbcid  3770  sbccow  3776  sbcco  3779  sbcco2  3780  sbcie2g  3794  eqsbc1  3800  sbcralt  3835  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  sbnfc2  4402  csbab  4403  csbie2df  4406  2nreu  4407  frpoins2fg  6317  isarep1OLD  6607  tfindes  7839  tfinds2  7840  frins2f  9706  iuninc  32489  suppss2f  32562  fmptdF  32580  disjdsct  32626  esumpfinvalf  34066  measiuns  34207  bnj580  34903  bnj985v  34943  bnj985  34944  xpab  35713  setinds2f  35767  bj-sbeq  36889  bj-sbel1  36893  bj-snsetex  36951  poimirlem25  37639  poimirlem26  37640  fdc1  37740  exlimddvfi  38116  frege52b  43878  frege58c  43910  pm13.194  44401  pm14.12  44410  sbiota1  44423  onfrALTlem1  44538  onfrALTlem1VD  44879  disjinfi  45186  ellimcabssub0  45615  2reu8i  47111  ich2exprop  47469  ichnreuop  47470  ichreuopeq  47471