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

Theorem dfsbcq 3155
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 3154 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 3156 instead of df-sbc 3154. (dfsbcq2 3156 is needed because unlike Quine we do not overload the df-sb 1659 syntax.) As a consequence of these theorems, we can derive sbc8g 3160, which is a weaker version of df-sbc 3154 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 3160, so we will allow direct use of df-sbc 3154 after theorem sbc2or 3161 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 2495 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3154 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3154 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 280 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   {cab 2421   [.wsbc 3153
This theorem is referenced by:  sbceq1d  3158  sbc8g  3160  spsbc  3165  sbcco  3175  sbcco2  3176  sbcie2g  3186  elrabsf  3191  eqsbc3  3192  csbeq1  3246  sbcnestgf  3290  sbcco3g  3297  cbvralcsf  3303  tfindes  4834  findes  4867  ralrnmpt  5870  findcard2  7340  ac6sfi  7343  indexfi  7406  ac6num  8351  fpwwe2cbv  8497  fpwwe2lem2  8499  fpwwe2lem3  8500  nn1suc  10013  uzindOLD  10356  uzind4s  10528  uzind4s2  10529  fzrevral  11123  fzshftral  11126  wrdind  11783  cjth  11900  prmind2  13082  isprs  14379  isdrs  14383  joinlem  14439  meetlem  14446  istos  14456  isdlat  14611  gsumvalx  14766  islmod  15946  elmptrab  17851  isfildlem  17881  quotval  20201  ifeqeqx  23993  sdclem2  26437  fdc  26440  fdc1  26441  sbccomieg  26840  rexrabdioph  26845  rexfrabdioph  26846  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  2nn0ind  26999  zindbi  27000  2sbc6g  27583  2sbc5g  27584  pm14.122b  27591  pm14.24  27600  iotavalsb  27601  sbiota1  27602  iotasbcq  27605  fvsb  27622  bnj609  29225  bnj601  29228  bnj944  29246  lshpkrlem3  29847  hdmap1ffval  32531  hdmap1fval  32532  hdmapffval  32564  hdmapfval  32565  hgmapffval  32623  hgmapfval  32624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431  df-sbc 3154
  Copyright terms: Public domain W3C validator