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

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3747, so we will allow direct use of df-sbc 3740 after Theorem sbc2or 3748 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 2825 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 3740 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 3740 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 313 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  {cab 2713  [wsbc 3739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-clel 2814  df-sbc 3740
This theorem is referenced by:  sbceq1d  3744  sbc8g  3747  spsbc  3752  sbccow  3762  sbcco  3765  sbcco2  3766  sbcie2g  3781  elrabsf  3787  eqsbc1  3788  csbeq1  3858  cbvralcsf  3900  sbcnestgfw  4378  sbcco3gw  4382  sbcnestgf  4383  sbcco3g  4387  csbie2df  4400  reusngf  4633  reuprg0  4663  sbcop  5446  reuop  6245  ralrnmptw  7043  ralrnmpt  7045  tfindes  7798  findcard2  9107  findcard2OLD  9227  ac6sfi  9230  indexfi  9303  nn1suc  12174  uzind4s2  12833  wrdind  14609  wrd2ind  14610  prmind2  16560  mndind  18637  elmptrab  23176  isfildlem  23206  ifeqeqx  31462  wrdt2ind  31802  bnj609  33520  bnj601  33523  sdclem2  36192  fdc1  36196  sbccom2  36575  sbccom2f  36576  sbccom2fi  36577  elimhyps  37414  dedths  37415  elimhyps2  37417  dedths2  37418  lshpkrlem3  37565  rexrabdioph  41095  rexfrabdioph  41096  2rexfrabdioph  41097  3rexfrabdioph  41098  4rexfrabdioph  41099  6rexfrabdioph  41100  7rexfrabdioph  41101  2nn0ind  41247  zindbi  41248  axfrege52c  42141  frege58c  42175  frege92  42209  2sbc6g  42677  2sbc5g  42678  pm14.122b  42685  pm14.24  42694  iotavalsb  42695  sbiota1  42696  fvsb  42714  or2expropbilem1  45238  ich2exprop  45635  reupr  45686
  Copyright terms: Public domain W3C validator