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

Theorem dfsbcq 2937
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 2936 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 2938 instead of df-sbc 2936. (dfsbcq2 2938 is needed because unlike Quine we do not overload the df-sb 1884 syntax.) As a consequence of these theorems, we can derive sbc8g 2942, which is a weaker version of df-sbc 2936 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 2942, so we will allow direct use of df-sbc 2936 after theorem sbc2or 2943 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 2316 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 2936 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 2936 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 281 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   {cab 2242   [.wsbc 2935
This theorem is referenced by:  sbceq1d  2940  sbc8g  2942  a4sbc  2947  sbcco  2957  sbcco2  2958  sbcie2g  2968  elrabsf  2973  eqsbc3  2974  csbeq1  3026  sbcnestgf  3070  sbcco3g  3078  cbvralcsf  3085  tfindes  4590  findes  4623  ralrnmpt  5568  findcard2  7031  ac6sfi  7034  indexfi  7096  ac6num  8039  fpwwe2cbv  8185  fpwwe2lem2  8187  fpwwe2lem3  8188  nn1suc  9700  uzindOLD  10038  uzind4s  10210  uzind4s2  10211  fzrevral  10797  fzshftral  10800  wrdind  11407  cjth  11518  prmind2  12696  isprs  13991  isdrs  13995  joinlem  14051  meetlem  14058  istos  14068  isdlat  14223  gsumvalx  14378  islmod  15558  elmptrab  17449  isfildlem  17479  quotval  19599  ifeqeqx  22959  sbcbidv2  24300  bisig0  25394  isibg2  25442  sdclem2  25784  fdc  25787  fdc1  25788  sbccomieg  26202  rexrabdioph  26207  rexfrabdioph  26208  2rexfrabdioph  26209  3rexfrabdioph  26210  4rexfrabdioph  26211  6rexfrabdioph  26212  7rexfrabdioph  26213  2nn0ind  26362  zindbi  26363  2sbc6g  26948  2sbc5g  26949  pm14.122b  26956  pm14.24  26965  iotavalsb  26966  sbiota1  26967  iotasbcq  26970  fvsb  26988  bnj609  27961  bnj601  27964  bnj944  27982  lshpkrlem3  28432  hdmap1ffval  31116  hdmap1fval  31117  hdmapffval  31149  hdmapfval  31150  hgmapffval  31208  hgmapfval  31209
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-cleq 2249  df-clel 2252  df-sbc 2936
  Copyright terms: Public domain W3C validator