Theorem dfsbcq 3780

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3786, so we will allow direct use of df-sbc 3779 after Theorem sbc2or 3787 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 2822	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}))
2		df-sbc 3779	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		df-sbc 3779	. 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})
4	1, 2, 3	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {cab 2710  [wsbc 3778

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 3779

This theorem is referenced by:  sbceq1d  3783  sbc8g  3786  spsbc  3791  sbccow  3801  sbcco  3804  sbcco2  3805  sbcie2g  3820  elrabsf  3826  eqsbc1  3827  csbeq1  3897  cbvralcsf  3939  sbcnestgfw  4419  sbcco3gw  4423  sbcnestgf  4424  sbcco3g  4428  csbie2df  4441  reusngf  4677  reuprg0  4707  sbcop  5490  reuop  6293  ralrnmptw  7096  ralrnmpt  7098  tfindes  7852  findcard2  9164  findcard2OLD  9284  ac6sfi  9287  indexfi  9360  nn1suc  12234  uzind4s2  12893  wrdind  14672  wrd2ind  14673  prmind2  16622  mndind  18709  elmptrab  23331  isfildlem  23361  ifeqeqx  31774  wrdt2ind  32117  bnj609  33928  bnj601  33931  sdclem2  36610  fdc1  36614  sbccom2  36993  sbccom2f  36994  sbccom2fi  36995  elimhyps  37831  dedths  37832  elimhyps2  37834  dedths2  37835  lshpkrlem3  37982  rexrabdioph  41532  rexfrabdioph  41533  2rexfrabdioph  41534  3rexfrabdioph  41535  4rexfrabdioph  41536  6rexfrabdioph  41537  7rexfrabdioph  41538  2nn0ind  41684  zindbi  41685  axfrege52c  42638  frege58c  42672  frege92  42706  2sbc6g  43174  2sbc5g  43175  pm14.122b  43182  pm14.24  43191  iotavalsb  43192  sbiota1  43193  fvsb  43211  or2expropbilem1  45742  ich2exprop  46139  reupr  46190