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

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3437, so we will allow direct use of df-sbc 3430 after theorem sbc2or 3438 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 2687 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 3430 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 3430 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 303 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  {cab 2606  [wsbc 3429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-clel 2616  df-sbc 3430
This theorem is referenced by:  sbceq1d  3434  sbc8g  3437  spsbc  3442  sbcco  3452  sbcco2  3453  sbcie2g  3463  elrabsf  3468  eqsbc3  3469  csbeq1  3529  cbvralcsf  3558  sbcnestgf  3986  sbcco3g  3990  ralrnmpt  6354  tfindes  7047  findcard2  8185  ac6sfi  8189  indexfi  8259  nn1suc  11026  uzind4s2  11734  wrdind  13458  wrd2ind  13459  prmind2  15379  mrcmndind  17347  elmptrab  21611  isfildlem  21642  ifeqeqx  29333  bnj609  30961  bnj601  30964  sdclem2  33509  fdc1  33513  sbccom2  33901  sbccom2f  33902  sbccom2fi  33903  elimhyps  34066  dedths  34067  elimhyps2  34069  dedths2  34070  lshpkrlem3  34218  rexrabdioph  37177  rexfrabdioph  37178  2rexfrabdioph  37179  3rexfrabdioph  37180  4rexfrabdioph  37181  6rexfrabdioph  37182  7rexfrabdioph  37183  2nn0ind  37329  zindbi  37330  axfrege52c  38001  frege58c  38035  frege92  38069  2sbc6g  38436  2sbc5g  38437  pm14.122b  38444  pm14.24  38453  iotavalsb  38454  sbiota1  38455  fvsb  38476
  Copyright terms: Public domain W3C validator