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

Theorem dfsbcq 2923
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 2922 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 2924 instead of df-sbc 2922. (dfsbcq2 2924 is needed because unlike Quine we do not overload the df-sb 1883 syntax.) As a consequence of these theorems, we can derive sbc8g 2928, which is a weaker version of df-sbc 2922 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 2928, so we will allow direct use of df-sbc 2922 after theorem sbc2or 2929 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 2313 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 2922 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 2922 . 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 2239   [.wsbc 2921
This theorem is referenced by:  sbceq1d  2926  sbc8g  2928  a4sbc  2933  sbcco  2943  sbcco2  2944  sbcie2g  2954  elrabsf  2959  eqsbc3  2960  csbeq1  3012  sbcnestgf  3056  sbcco3g  3064  cbvralcsf  3071  tfindes  4544  findes  4577  ralrnmpt  5521  findcard2  6983  ac6sfi  6986  indexfi  7047  ac6num  7990  fpwwe2cbv  8132  fpwwe2lem2  8134  fpwwe2lem3  8135  nn1suc  9647  uzindOLD  9985  uzind4s  10157  uzind4s2  10158  fzrevral  10744  fzshftral  10747  wrdind  11354  cjth  11465  prmind2  12643  isprs  13908  isdrs  13912  joinlem  13968  meetlem  13975  istos  13985  isdlat  14131  gsumvalx  14286  islmod  15466  elmptrab  17354  isfildlem  17384  quotval  19504  sbcbidv2  24134  bisig0  25228  isibg2  25276  sdclem2  25618  fdc  25621  fdc1  25622  sbccomieg  26036  rexrabdioph  26041  rexfrabdioph  26042  2rexfrabdioph  26043  3rexfrabdioph  26044  4rexfrabdioph  26045  6rexfrabdioph  26046  7rexfrabdioph  26047  2nn0ind  26196  zindbi  26197  2sbc6g  26782  2sbc5g  26783  pm14.122b  26790  pm14.24  26799  iotavalsb  26800  sbiota1  26801  iotasbcq  26804  fvsb  26822  bnj609  27638  bnj601  27641  bnj944  27659  lshpkrlem3  28061  hdmap1ffval  30745  hdmap1fval  30746  hdmapffval  30778  hdmapfval  30779  hgmapffval  30837  hgmapfval  30838
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 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-cleq 2246  df-clel 2249  df-sbc 2922
  Copyright terms: Public domain W3C validator