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

Theorem dfsbcq 3280
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 3279 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 3281 instead of df-sbc 3279. (dfsbcq2 3281 is needed because unlike Quine we do not overload the df-sb 1808 syntax.) As a consequence of these theorems, we can derive sbc8g 3286, which is a weaker version of df-sbc 3279 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 3286, so we will allow direct use of df-sbc 3279 after theorem sbc2or 3287 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 2527 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3279 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3279 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 296 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1454    e. wcel 1897   {cab 2447   [.wsbc 3278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-cleq 2454  df-clel 2457  df-sbc 3279
This theorem is referenced by:  sbceq1d  3283  sbc8g  3286  spsbc  3291  sbcco  3301  sbcco2  3302  sbcie2g  3312  elrabsf  3317  eqsbc3  3318  csbeq1  3377  cbvralcsf  3406  sbcnestgf  3795  sbcco3g  3799  ralrnmpt  6053  tfindes  6715  findcard2  7836  ac6sfi  7840  indexfi  7907  nn1suc  10657  uzind4s2  11248  wrdind  12869  wrd2ind  12870  prmind2  14683  mrcmndind  16661  elmptrab  20890  isfildlem  20920  ifeqeqx  28206  bnj609  29776  bnj601  29779  sdclem2  32115  fdc1  32119  sbccom2  32409  sbccom2f  32410  sbccom2fi  32411  elimhyps  32577  dedths  32578  elimhyps2  32580  dedths2  32581  lshpkrlem3  32722  rexrabdioph  35681  rexfrabdioph  35682  2rexfrabdioph  35683  3rexfrabdioph  35684  4rexfrabdioph  35685  6rexfrabdioph  35686  7rexfrabdioph  35687  2nn0ind  35837  zindbi  35838  axfrege52c  36527  frege58c  36561  frege92  36595  2sbc6g  36809  2sbc5g  36810  pm14.122b  36817  pm14.24  36826  iotavalsb  36827  sbiota1  36828  fvsb  36848
  Copyright terms: Public domain W3C validator