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

Theorem dfsbcq 2994
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 2993 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 2995 instead of df-sbc 2993. (dfsbcq2 2995 is needed because unlike Quine we do not overload the df-sb 1636 syntax.) As a consequence of these theorems, we can derive sbc8g 2999, which is a weaker version of df-sbc 2993 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 2999, so we will allow direct use of df-sbc 2993 after theorem sbc2or 3000 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 2344 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 2993 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 2993 . 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 1628    e. wcel 1688   {cab 2270   [.wsbc 2992
This theorem is referenced by:  sbceq1d  2997  sbc8g  2999  spsbc  3004  sbcco  3014  sbcco2  3015  sbcie2g  3025  elrabsf  3030  eqsbc3  3031  csbeq1  3085  sbcnestgf  3129  sbcco3g  3137  cbvralcsf  3144  tfindes  4652  findes  4685  ralrnmpt  5630  findcard2  7093  ac6sfi  7096  indexfi  7158  ac6num  8101  fpwwe2cbv  8247  fpwwe2lem2  8249  fpwwe2lem3  8250  nn1suc  9762  uzindOLD  10101  uzind4s  10273  uzind4s2  10274  fzrevral  10860  fzshftral  10863  wrdind  11471  cjth  11582  prmind2  12763  isprs  14058  isdrs  14062  joinlem  14118  meetlem  14125  istos  14135  isdlat  14290  gsumvalx  14445  islmod  15625  elmptrab  17516  isfildlem  17546  quotval  19666  ifeqeqx  23026  sbcbidv2  24367  bisig0  25461  isibg2  25509  sdclem2  25851  fdc  25854  fdc1  25855  sbccomieg  26269  rexrabdioph  26274  rexfrabdioph  26275  2rexfrabdioph  26276  3rexfrabdioph  26277  4rexfrabdioph  26278  6rexfrabdioph  26279  7rexfrabdioph  26280  2nn0ind  26429  zindbi  26430  2sbc6g  27014  2sbc5g  27015  pm14.122b  27022  pm14.24  27031  iotavalsb  27032  sbiota1  27033  iotasbcq  27036  fvsb  27054  bnj609  28216  bnj601  28219  bnj944  28237  lshpkrlem3  28569  hdmap1ffval  31253  hdmap1fval  31254  hdmapffval  31286  hdmapfval  31287  hgmapffval  31345  hgmapfval  31346
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-cleq 2277  df-clel 2280  df-sbc 2993
  Copyright terms: Public domain W3C validator