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

Theorem dfsbcq 3209
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 3208 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 3210 instead of df-sbc 3208. (dfsbcq2 3210 is needed because unlike Quine we do not overload the df-sb 1701 syntax.) As a consequence of these theorems, we can derive sbc8g 3215, which is a weaker version of df-sbc 3208 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 3215, so we will allow direct use of df-sbc 3208 after theorem sbc2or 3216 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 2503 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3208 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3208 . 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 1369    e. wcel 1756   {cab 2429   [.wsbc 3207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439  df-sbc 3208
This theorem is referenced by:  sbceq1d  3212  sbc8g  3215  spsbc  3220  sbcco  3230  sbcco2  3231  sbcie2g  3241  elrabsf  3246  eqsbc3  3247  csbeq1  3312  cbvralcsf  3340  sbcnestgf  3712  sbcco3g  3716  ralrnmpt  5873  tfindes  6494  findes  6527  findcard2  7573  ac6sfi  7577  indexfi  7640  ac6num  8669  fpwwe2cbv  8818  fpwwe2lem2  8820  fpwwe2lem3  8821  nn1suc  10364  uzindOLD  10757  uzind4s  10935  uzind4s2  10936  fzrevral  11565  fzshftral  11568  wrdind  12392  wrd2ind  12393  cjth  12613  prmind2  13795  isprs  15121  isdrs  15125  istos  15226  isdlat  15384  mrcmndind  15515  gsumvalx  15523  islmod  16974  elmptrab  19422  isfildlem  19452  quotval  21780  ifeqeqx  25924  nn0min  26112  sdclem2  28664  fdc  28667  fdc1  28668  sbccom2  28960  sbccom2f  28961  sbccom2fi  28962  sbccomieg  29157  rexrabdioph  29158  rexfrabdioph  29159  2rexfrabdioph  29160  3rexfrabdioph  29161  4rexfrabdioph  29162  6rexfrabdioph  29163  7rexfrabdioph  29164  2nn0ind  29312  zindbi  29313  2sbc6g  29695  2sbc5g  29696  pm14.122b  29703  pm14.24  29712  iotavalsb  29713  sbiota1  29714  iotasbcq  29717  fvsb  29734  bnj609  32006  bnj601  32009  bnj944  32027  elimhyps  32708  dedths  32709  elimhyps2  32711  dedths2  32712  lshpkrlem3  32853  hdmap1ffval  35537  hdmap1fval  35538  hdmapffval  35570  hdmapfval  35571  hgmapffval  35629  hgmapfval  35630
  Copyright terms: Public domain W3C validator