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

Theorem dfsbcq 3307
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 3306 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 3308 instead of df-sbc 3306. (dfsbcq2 3308 is needed because unlike Quine we do not overload the df-sb 1790 syntax.) As a consequence of these theorems, we can derive sbc8g 3313, which is a weaker version of df-sbc 3306 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 3313, so we will allow direct use of df-sbc 3306 after theorem sbc2or 3314 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 2501 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3306 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3306 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 291 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1870   {cab 2414   [.wsbc 3305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2421  df-clel 2424  df-sbc 3306
This theorem is referenced by:  sbceq1d  3310  sbc8g  3313  spsbc  3318  sbcco  3328  sbcco2  3329  sbcie2g  3339  elrabsf  3344  eqsbc3  3345  csbeq1  3404  cbvralcsf  3433  sbcnestgf  3818  sbcco3g  3822  ralrnmpt  6046  tfindes  6703  findcard2  7817  ac6sfi  7821  indexfi  7888  nn1suc  10630  uzind4s2  11220  wrdind  12818  wrd2ind  12819  prmind2  14606  mrcmndind  16564  elmptrab  20773  isfildlem  20803  ifeqeqx  27997  bnj609  29516  bnj601  29519  sdclem2  31778  fdc1  31782  sbccom2  32072  sbccom2f  32073  sbccom2fi  32074  elimhyps  32245  dedths  32246  elimhyps2  32248  dedths2  32249  lshpkrlem3  32390  rexrabdioph  35349  rexfrabdioph  35350  2rexfrabdioph  35351  3rexfrabdioph  35352  4rexfrabdioph  35353  6rexfrabdioph  35354  7rexfrabdioph  35355  2nn0ind  35502  zindbi  35503  axfrege52c  36123  frege58c  36157  frege92  36191  2sbc6g  36406  2sbc5g  36407  pm14.122b  36414  pm14.24  36423  iotavalsb  36424  sbiota1  36425  fvsb  36445
  Copyright terms: Public domain W3C validator