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

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3748, so we will allow direct use of df-sbc 3741 after Theorem sbc2or 3749 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 2822 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 3741 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 3741 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 314 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  {cab 2710  [wsbc 3740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-sbc 3741
This theorem is referenced by:  sbceq1d  3745  sbc8g  3748  spsbc  3753  sbccow  3763  sbcco  3766  sbcco2  3767  sbcie2g  3782  elrabsf  3788  eqsbc1  3789  csbeq1  3859  cbvralcsf  3901  sbcnestgfw  4379  sbcco3gw  4383  sbcnestgf  4384  sbcco3g  4388  csbie2df  4401  reusngf  4634  reuprg0  4664  sbcop  5447  reuop  6246  ralrnmptw  7045  ralrnmpt  7047  tfindes  7800  findcard2  9111  findcard2OLD  9231  ac6sfi  9234  indexfi  9307  nn1suc  12180  uzind4s2  12839  wrdind  14616  wrd2ind  14617  prmind2  16566  mndind  18643  elmptrab  23194  isfildlem  23224  ifeqeqx  31507  wrdt2ind  31856  bnj609  33586  bnj601  33589  sdclem2  36247  fdc1  36251  sbccom2  36630  sbccom2f  36631  sbccom2fi  36632  elimhyps  37469  dedths  37470  elimhyps2  37472  dedths2  37473  lshpkrlem3  37620  rexrabdioph  41160  rexfrabdioph  41161  2rexfrabdioph  41162  3rexfrabdioph  41163  4rexfrabdioph  41164  6rexfrabdioph  41165  7rexfrabdioph  41166  2nn0ind  41312  zindbi  41313  axfrege52c  42247  frege58c  42281  frege92  42315  2sbc6g  42783  2sbc5g  42784  pm14.122b  42791  pm14.24  42800  iotavalsb  42801  sbiota1  42802  fvsb  42820  or2expropbilem1  45352  ich2exprop  45749  reupr  45800
  Copyright terms: Public domain W3C validator