MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbsbc Structured version   Unicode version

Theorem sbsbc 3167
Description: Show that df-sb 1660 and df-sbc 3164 are equivalent when the class term  A in df-sbc 3164 is a set variable. This theorem lets us reuse theorems based on df-sb 1660 for proofs involving df-sbc 3164. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.)
Assertion
Ref Expression
sbsbc  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )

Proof of Theorem sbsbc
StepHypRef Expression
1 eqid 2438 . 2  |-  y  =  y
2 dfsbcq2 3166 . 2  |-  ( y  =  y  ->  ( [ y  /  x ] ph  <->  [. y  /  x ]. ph ) )
31, 2ax-mp 8 1  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   [wsb 1659   [.wsbc 3163
This theorem is referenced by:  spsbc  3175  sbcid  3179  sbcco  3185  sbcco2  3186  sbcie2g  3196  eqsbc3  3202  sbcralt  3235  sbnfc2  3311  csbabg  3312  cbvralcsf  3313  cbvreucsf  3315  cbvrabcsf  3316  tfindes  4844  tfinds2  4845  isarep1  5534  iuninc  24013  suppss2f  24051  fmptdF  24071  disjdsct  24092  esumpfinvalf  24468  measiuns  24573  setinds2f  25408  wfis2fg  25488  frins2fg  25524  fdc1  26452  pm13.194  27591  pm14.12  27600  sbiota1  27613  onfrALTlem1  28696  onfrALTlem1VD  29064  bnj580  29346  bnj985  29386
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-clab 2425  df-cleq 2431  df-clel 2434  df-sbc 3164
  Copyright terms: Public domain W3C validator