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

Theorem dfsbcq 3006
Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, provides us with a weak definition of the proper substitution of a class for a set. Since our df-sbc 3005 does not result in the same behavior as Quine's for proper classes, if we wished to avoid conflict with Quine's definition we could start with this theorem and dfsbcq2 3007 instead of df-sbc 3005. (dfsbcq2 3007 is needed because unlike Quine we do not overload the df-sb 1639 syntax.) As a consequence of these theorems, we can derive sbc8g 3011, which is a weaker version of df-sbc 3005 that leaves substitution undefined when  A is a proper class.

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3011, so we will allow direct use of df-sbc 3005 after theorem sbc2or 3012 below. Proper substiution with a proper class is rarely needed, and when it is, we can simply use the expansion of Quine's definition. (Contributed by NM, 14-Apr-1995.)

Assertion
Ref Expression
dfsbcq  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )

Proof of Theorem dfsbcq
StepHypRef Expression
1 eleq1 2356 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3005 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3005 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 279 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   {cab 2282   [.wsbc 3004
This theorem is referenced by:  sbceq1d  3009  sbc8g  3011  spsbc  3016  sbcco  3026  sbcco2  3027  sbcie2g  3037  elrabsf  3042  eqsbc3  3043  csbeq1  3097  sbcnestgf  3141  sbcco3g  3149  cbvralcsf  3156  tfindes  4669  findes  4702  ralrnmpt  5685  findcard2  7114  ac6sfi  7117  indexfi  7179  ac6num  8122  fpwwe2cbv  8268  fpwwe2lem2  8270  fpwwe2lem3  8271  nn1suc  9783  uzindOLD  10122  uzind4s  10294  uzind4s2  10295  fzrevral  10882  fzshftral  10885  wrdind  11493  cjth  11604  prmind2  12785  isprs  14080  isdrs  14084  joinlem  14140  meetlem  14147  istos  14157  isdlat  14312  gsumvalx  14467  islmod  15647  elmptrab  17538  isfildlem  17568  quotval  19688  ifeqeqx  23050  sbcbidv2  25072  bisig0  26165  isibg2  26213  sdclem2  26555  fdc  26558  fdc1  26559  sbccomieg  26973  rexrabdioph  26978  rexfrabdioph  26979  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  2nn0ind  27133  zindbi  27134  2sbc6g  27718  2sbc5g  27719  pm14.122b  27726  pm14.24  27735  iotavalsb  27736  sbiota1  27737  iotasbcq  27740  fvsb  27758  bnj609  29265  bnj601  29268  bnj944  29286  lshpkrlem3  29924  hdmap1ffval  32608  hdmap1fval  32609  hdmapffval  32641  hdmapfval  32642  hgmapffval  32700  hgmapfval  32701
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-cleq 2289  df-clel 2292  df-sbc 3005
  Copyright terms: Public domain W3C validator