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

Theorem dfsbcq 3329
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 3328 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 3330 instead of df-sbc 3328. (dfsbcq2 3330 is needed because unlike Quine we do not overload the df-sb 1740 syntax.) As a consequence of these theorems, we can derive sbc8g 3335, which is a weaker version of df-sbc 3328 that leaves substitution undefined when is a proper class.

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3335, so we will allow direct use of df-sbc 3328 after theorem sbc2or 3336 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

Proof of Theorem dfsbcq
StepHypRef Expression
1 eleq1 2529 . 2
2 df-sbc 3328 . 2
3 df-sbc 3328 . 2
41, 2, 33bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {cab 2442  [.wsbc 3327
This theorem is referenced by:  sbceq1d  3332  sbc8g  3335  spsbc  3340  sbcco  3350  sbcco2  3351  sbcie2g  3361  elrabsf  3366  eqsbc3  3367  csbeq1  3437  cbvralcsf  3466  sbcnestgf  3839  sbcco3g  3843  ralrnmpt  6040  tfindes  6697  findcard2  7780  ac6sfi  7784  indexfi  7848  nn1suc  10582  uzindOLD  10982  uzind4s2  11171  wrdind  12702  wrd2ind  12703  prmind2  14228  mrcmndind  15997  elmptrab  20328  isfildlem  20358  ifeqeqx  27419  sdclem2  30235  fdc1  30239  sbccom2  30530  sbccom2f  30531  sbccom2fi  30532  rexrabdioph  30727  rexfrabdioph  30728  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  2nn0ind  30881  zindbi  30882  2sbc6g  31322  2sbc5g  31323  pm14.122b  31330  pm14.24  31339  iotavalsb  31340  sbiota1  31341  fvsb  31361  bnj609  33975  bnj601  33978  elimhyps  34692  dedths  34693  elimhyps2  34695  dedths2  34696  lshpkrlem3  34837  axfrege52c  37914  frege58c  37948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-sbc 3328
  Copyright terms: Public domain W3C validator