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

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3404, so we will allow direct use of df-sbc 3397 after theorem sbc2or 3405 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 2670 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 3397 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 3397 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 301 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1975  {cab 2590  [wsbc 3396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2597  df-clel 2600  df-sbc 3397
This theorem is referenced by:  sbceq1d  3401  sbc8g  3404  spsbc  3409  sbcco  3419  sbcco2  3420  sbcie2g  3430  elrabsf  3435  eqsbc3  3436  csbeq1  3496  cbvralcsf  3525  sbcnestgf  3941  sbcco3g  3945  ralrnmpt  6256  tfindes  6926  findcard2  8057  ac6sfi  8061  indexfi  8129  nn1suc  10883  uzind4s2  11576  wrdind  13269  wrd2ind  13270  prmind2  15177  mrcmndind  17130  elmptrab  21377  isfildlem  21408  ifeqeqx  28546  bnj609  30042  bnj601  30045  sdclem2  32506  fdc1  32510  sbccom2  32898  sbccom2f  32899  sbccom2fi  32900  elimhyps  33063  dedths  33064  elimhyps2  33066  dedths2  33067  lshpkrlem3  33215  rexrabdioph  36174  rexfrabdioph  36175  2rexfrabdioph  36176  3rexfrabdioph  36177  4rexfrabdioph  36178  6rexfrabdioph  36179  7rexfrabdioph  36180  2nn0ind  36326  zindbi  36327  axfrege52c  36999  frege58c  37033  frege92  37067  2sbc6g  37436  2sbc5g  37437  pm14.122b  37444  pm14.24  37453  iotavalsb  37454  sbiota1  37455  fvsb  37475
  Copyright terms: Public domain W3C validator