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

Theorem sbsbc 2995
Description: Show that df-sb 1630 and df-sbc 2992 are equivalent when the class term  A in df-sbc 2992 is a set variable. This theorem lets us reuse theorems based on df-sb 1630 for proofs involving df-sbc 2992. (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 2283 . 2  |-  y  =  y
2 dfsbcq2 2994 . 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 1629   [.wsbc 2991
This theorem is referenced by:  spsbc  3003  sbcid  3007  sbcco  3013  sbcco2  3014  sbcie2g  3024  eqsbc3  3030  sbcralt  3063  csbid  3088  sbnfc2  3141  csbabg  3142  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  tfindes  4653  tfinds2  4654  isarep1  5331  setinds2f  23546  wfis2fg  23622  frins2fg  23658  isconcl5a  25513  isconcl5ab  25514  fdc1  25868  pm13.194  27024  pm14.12  27033  sbiota1  27046  onfrALTlem1  27686  onfrALTlem1VD  28039  bnj605  28312  bnj580  28318  bnj985  28358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992
  Copyright terms: Public domain W3C validator