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

Theorem dfsbcq 3333
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 3332 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 3334 instead of df-sbc 3332. (dfsbcq2 3334 is needed because unlike Quine we do not overload the df-sb 1712 syntax.) As a consequence of these theorems, we can derive sbc8g 3339, which is a weaker version of df-sbc 3332 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 3339, so we will allow direct use of df-sbc 3332 after theorem sbc2or 3340 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 2539 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3332 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3332 . 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 1379    e. wcel 1767   {cab 2452   [.wsbc 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462  df-sbc 3332
This theorem is referenced by:  sbceq1d  3336  sbc8g  3339  spsbc  3344  sbcco  3354  sbcco2  3355  sbcie2g  3365  elrabsf  3370  eqsbc3  3371  csbeq1  3438  cbvralcsf  3467  sbcnestgf  3839  sbcco3g  3843  ralrnmpt  6031  tfindes  6682  findes  6715  findcard2  7761  ac6sfi  7765  indexfi  7829  ac6num  8860  fpwwe2cbv  9009  fpwwe2lem2  9011  fpwwe2lem3  9012  nn1suc  10558  uzindOLD  10956  uzind4s  11142  uzind4s2  11143  fzrevral  11763  fzshftral  11766  wrdind  12668  wrd2ind  12669  cjth  12902  prmind2  14090  isprs  15420  isdrs  15424  istos  15525  isdlat  15683  mrcmndind  15819  gsumvalx  15827  islmod  17328  elmptrab  20155  isfildlem  20185  quotval  22514  ifeqeqx  27190  nn0min  27376  sdclem2  30065  fdc  30068  fdc1  30069  sbccom2  30361  sbccom2f  30362  sbccom2fi  30363  sbccomieg  30557  rexrabdioph  30558  rexfrabdioph  30559  2rexfrabdioph  30560  3rexfrabdioph  30561  4rexfrabdioph  30562  6rexfrabdioph  30563  7rexfrabdioph  30564  2nn0ind  30712  zindbi  30713  2sbc6g  31127  2sbc5g  31128  pm14.122b  31135  pm14.24  31144  iotavalsb  31145  sbiota1  31146  iotasbcq  31149  fvsb  31166  bnj609  33271  bnj601  33274  bnj944  33292  elimhyps  33981  dedths  33982  elimhyps2  33984  dedths2  33985  lshpkrlem3  34126  hdmap1ffval  36810  hdmap1fval  36811  hdmapffval  36843  hdmapfval  36844  hgmapffval  36902  hgmapfval  36903  frege52c  37121
  Copyright terms: Public domain W3C validator