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

Theorem sbsbc 3008
Description: Show that df-sb 1639 and df-sbc 3005 are equivalent when the class term  A in df-sbc 3005 is a set variable. This theorem lets us reuse theorems based on df-sb 1639 for proofs involving df-sbc 3005. (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 2296 . 2  |-  y  =  y
2 dfsbcq2 3007 . 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 176   [wsb 1638   [.wsbc 3004
This theorem is referenced by:  spsbc  3016  sbcid  3020  sbcco  3026  sbcco2  3027  sbcie2g  3037  eqsbc3  3043  sbcralt  3076  csbid  3101  sbnfc2  3154  csbabg  3155  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  tfindes  4669  tfinds2  4670  isarep1  5347  iuninc  23174  suppss2f  23216  fmptdF  23236  disjdsct  23384  esumpfinvalf  23459  setinds2f  24206  wfis2fg  24282  frins2fg  24318  isconcl5a  26204  isconcl5ab  26205  fdc1  26559  pm13.194  27715  pm14.12  27724  sbiota1  27737  onfrALTlem1  28612  onfrALTlem1VD  28982  bnj605  29255  bnj580  29261  bnj985  29301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-clab 2283  df-cleq 2289  df-clel 2292  df-sbc 3005
  Copyright terms: Public domain W3C validator