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

Theorem dfsbcq 3179
Description: Proper substitution of a class for a set in a wff given equal classes. This is the essence of the sixth axiom of Frege, specifically Proposition 52 of [Frege1879] p. 50.

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 3178 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 3180 instead of df-sbc 3178. (dfsbcq2 3180 is needed because unlike Quine we do not overload the df-sb 1702 syntax.) As a consequence of these theorems, we can derive sbc8g 3184, which is a weaker version of df-sbc 3178 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 3184, so we will allow direct use of df-sbc 3178 after theorem sbc2or 3185 below. Proper substitution 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 3178 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3178 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 288 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1364    e. wcel 1757   {cab 2421   [.wsbc 3177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-12 1793  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2428  df-clel 2431  df-sbc 3178
This theorem is referenced by:  sbceq1d  3182  sbc8g  3184  spsbc  3189  sbcco  3199  sbcco2  3200  sbcie2g  3210  elrabsf  3215  eqsbc3  3216  csbeq1  3281  cbvralcsf  3309  sbcnestgf  3681  sbcco3g  3685  ralrnmpt  5842  tfindes  6464  findes  6497  findcard2  7542  ac6sfi  7546  indexfi  7609  ac6num  8638  fpwwe2cbv  8787  fpwwe2lem2  8789  fpwwe2lem3  8790  nn1suc  10333  uzindOLD  10726  uzind4s  10904  uzind4s2  10905  fzrevral  11530  fzshftral  11533  wrdind  12357  wrd2ind  12358  cjth  12578  prmind2  13759  isprs  15085  isdrs  15089  istos  15190  isdlat  15348  mrcmndind  15478  gsumvalx  15486  islmod  16878  elmptrab  19244  isfildlem  19274  quotval  21645  ifeqeqx  25728  nn0min  25915  sdclem2  28484  fdc  28487  fdc1  28488  sbccom2  28780  sbccom2f  28781  sbccom2fi  28782  sbccomieg  28978  rexrabdioph  28979  rexfrabdioph  28980  2rexfrabdioph  28981  3rexfrabdioph  28982  4rexfrabdioph  28983  6rexfrabdioph  28984  7rexfrabdioph  28985  2nn0ind  29133  zindbi  29134  2sbc6g  29516  2sbc5g  29517  pm14.122b  29524  pm14.24  29533  iotavalsb  29534  sbiota1  29535  iotasbcq  29538  fvsb  29555  bnj609  31652  bnj601  31655  bnj944  31673  elimhyps  32225  dedths  32226  elimhyps2  32228  dedths2  32229  lshpkrlem3  32370  hdmap1ffval  35054  hdmap1fval  35055  hdmapffval  35087  hdmapfval  35088  hgmapffval  35146  hgmapfval  35147
  Copyright terms: Public domain W3C validator