Theorem dfsbcq 3746

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3752, so we will allow direct use of df-sbc 3745 after Theorem sbc2or 3753 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

Step	Hyp	Ref	Expression
1		eleq1 2849	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}))
2		df-sbc 3745	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		df-sbc 3745	. 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})
4	1, 2, 3	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  {cab 2739  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836  df-sbc 3745

This theorem is referenced by:  sbceq1d  3749  sbc8g  3752  spsbc  3757  sbccow  3767  sbcco  3770  sbcco2  3771  sbcie2g  3784  elrabsf  3789  eqsbc1  3790  csbeq1  3855  cbvralcsf  3894  sbcnestgfw  4374  sbcco3gw  4378  sbcnestgf  4379  sbcco3g  4383  csbie2df  4396  reusngf  4632  reuprg0  4660  sbcop  5456  reuop  6274  ralrnmptw  7069  ralrnmpt  7071  tfindes  7837  findcard2  9127  ac6sfi  9222  indexfi  9298  nn1suc  12227  uzind4s2  12905  wrdind  14730  wrd2ind  14731  prmind2  16700  mndind  18843  elmptrab  23865  isfildlem  23895  ifeqeqx  32688  wrdt2ind  33090  bnj609  35174  bnj601  35177  weiunlem  36776  sdclem2  38194  fdc1  38198  sbccom2  38577  sbccom2f  38578  sbccom2fi  38579  elimhyps  39538  dedths  39539  elimhyps2  39541  dedths2  39542  lshpkrlem3  39689  rexrabdioph  43324  rexfrabdioph  43325  2rexfrabdioph  43326  3rexfrabdioph  43327  4rexfrabdioph  43328  6rexfrabdioph  43329  7rexfrabdioph  43330  2nn0ind  43475  zindbi  43476  axfrege52c  44416  frege58c  44450  frege92  44484  2sbc6g  44944  2sbc5g  44945  pm14.122b  44952  pm14.24  44961  iotavalsb  44962  sbiota1  44963  fvsb  44980  or2expropbilem1  47579  ich2exprop  48030  reupr  48081