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

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3476, so we will allow direct use of df-sbc 3469 after theorem sbc2or 3477 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 2718 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 3469 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 3469 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 303 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030  {cab 2637  [wsbc 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647  df-sbc 3469
This theorem is referenced by:  sbceq1d  3473  sbc8g  3476  spsbc  3481  sbcco  3491  sbcco2  3492  sbcie2g  3502  elrabsf  3507  eqsbc3  3508  csbeq1  3569  cbvralcsf  3598  sbcnestgf  4028  sbcco3g  4032  ralrnmpt  6408  tfindes  7104  findcard2  8241  ac6sfi  8245  indexfi  8315  nn1suc  11079  uzind4s2  11787  wrdind  13522  wrd2ind  13523  prmind2  15445  mrcmndind  17413  elmptrab  21678  isfildlem  21708  ifeqeqx  29487  bnj609  31113  bnj601  31116  sdclem2  33668  fdc1  33672  sbccom2  34060  sbccom2f  34061  sbccom2fi  34062  elimhyps  34565  dedths  34566  elimhyps2  34568  dedths2  34569  lshpkrlem3  34717  rexrabdioph  37675  rexfrabdioph  37676  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  2nn0ind  37827  zindbi  37828  axfrege52c  38498  frege58c  38532  frege92  38566  2sbc6g  38933  2sbc5g  38934  pm14.122b  38941  pm14.24  38950  iotavalsb  38951  sbiota1  38952  fvsb  38973
  Copyright terms: Public domain W3C validator