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

Theorem dfsbcq 3237
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 3236 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 3238 instead of df-sbc 3236. (dfsbcq2 3238 is needed because unlike Quine we do not overload the df-sb 1791 syntax.) As a consequence of these theorems, we can derive sbc8g 3243, which is a weaker version of df-sbc 3236 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 3243, so we will allow direct use of df-sbc 3236 after theorem sbc2or 3244 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 2488 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3236 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3236 . 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 1872   {cab 2408   [.wsbc 3235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-cleq 2415  df-clel 2418  df-sbc 3236
This theorem is referenced by:  sbceq1d  3240  sbc8g  3243  spsbc  3248  sbcco  3258  sbcco2  3259  sbcie2g  3269  elrabsf  3274  eqsbc3  3275  csbeq1  3334  cbvralcsf  3363  sbcnestgf  3750  sbcco3g  3754  ralrnmpt  5983  tfindes  6640  findcard2  7757  ac6sfi  7761  indexfi  7828  nn1suc  10574  uzind4s2  11164  wrdind  12772  wrd2ind  12773  prmind2  14571  mrcmndind  16549  elmptrab  20777  isfildlem  20807  ifeqeqx  28097  bnj609  29673  bnj601  29676  sdclem2  31972  fdc1  31976  sbccom2  32266  sbccom2f  32267  sbccom2fi  32268  elimhyps  32439  dedths  32440  elimhyps2  32442  dedths2  32443  lshpkrlem3  32584  rexrabdioph  35543  rexfrabdioph  35544  2rexfrabdioph  35545  3rexfrabdioph  35546  4rexfrabdioph  35547  6rexfrabdioph  35548  7rexfrabdioph  35549  2nn0ind  35700  zindbi  35701  axfrege52c  36390  frege58c  36424  frege92  36458  2sbc6g  36673  2sbc5g  36674  pm14.122b  36681  pm14.24  36690  iotavalsb  36691  sbiota1  36692  fvsb  36712
  Copyright terms: Public domain W3C validator