Theorem sbsbc 3439

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

Assertion

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

Proof of Theorem sbsbc

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

Syntax hints:   ↔ wb 196  [wsb 1880  [wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  spsbc  3448  sbcid  3452  sbcco  3458  sbcco2  3459  sbcie2g  3469  eqsbc3  3475  sbcralt  3510  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  sbnfc2  4007  csbab  4008  wfis2fg  5717  isarep1  5977  tfindes  7062  tfinds2  7063  iuninc  29379  suppss2f  29439  fmptdF  29456  disjdsct  29480  esumpfinvalf  30138  measiuns  30280  bnj580  30983  bnj985  31023  setinds2f  31684  frins2fg  31744  bj-sbeq  32896  bj-sbel1  32900  bj-snsetex  32951  poimirlem25  33434  poimirlem26  33435  fdc1  33542  exlimddvfi  33927  frege52b  38183  frege58c  38215  pm13.194  38613  pm14.12  38622  sbiota1  38635  onfrALTlem1  38763  csbabgOLD  39050  onfrALTlem1VD  39126  disjinfi  39380  ellimcabssub0  39849