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

Theorem dfsbcq 3722
 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 3721 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 3723 instead of df-sbc 3721. (dfsbcq2 3723 is needed because unlike Quine we do not overload the df-sb 2070 syntax.) As a consequence of these theorems, we can derive sbc8g 3728, which is a weaker version of df-sbc 3721 that leaves substitution undefined when 𝐴 is a proper class. However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3728, so we will allow direct use of df-sbc 3721 after theorem sbc2or 3729 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 2877 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 3721 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 3721 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 317 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {cab 2776  [wsbc 3720 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-sbc 3721 This theorem is referenced by:  sbceq1d  3725  sbc8g  3728  spsbc  3733  sbccow  3743  sbcco  3746  sbcco2  3747  sbcie2g  3759  elrabsf  3764  eqsbc3  3765  csbeq1  3831  cbvralcsf  3870  sbcnestgfw  4326  sbcco3gw  4330  sbcnestgf  4331  sbcco3g  4335  csbie2df  4348  reusngf  4572  reuprg0  4598  sbcop  5346  reuop  6113  ralrnmptw  6838  ralrnmpt  6840  tfindes  7560  findcard2  8745  ac6sfi  8749  indexfi  8819  nn1suc  11650  uzind4s2  12300  wrdind  14078  wrd2ind  14079  prmind2  16022  mndind  17987  elmptrab  22442  isfildlem  22472  ifeqeqx  30319  wrdt2ind  30663  bnj609  32314  bnj601  32317  sdclem2  35199  fdc1  35203  sbccom2  35582  sbccom2f  35583  sbccom2fi  35584  elimhyps  36276  dedths  36277  elimhyps2  36279  dedths2  36280  lshpkrlem3  36427  rexrabdioph  39778  rexfrabdioph  39779  2rexfrabdioph  39780  3rexfrabdioph  39781  4rexfrabdioph  39782  6rexfrabdioph  39783  7rexfrabdioph  39784  2nn0ind  39929  zindbi  39930  axfrege52c  40631  frege58c  40665  frege92  40699  2sbc6g  41162  2sbc5g  41163  pm14.122b  41170  pm14.24  41179  iotavalsb  41180  sbiota1  41181  fvsb  41199  or2expropbilem1  43667  ich2exprop  44031  reupr  44082
 Copyright terms: Public domain W3C validator