Theorem dfsbcq 3642

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

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637   ∈ wcel 2157  {cab 2799  [wsbc 3640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2806  df-clel 2809  df-sbc 3641

This theorem is referenced by:  sbceq1d  3645  sbc8g  3648  spsbc  3653  sbcco  3663  sbcco2  3664  sbcie2g  3674  elrabsf  3679  eqsbc3  3680  csbeq1  3738  cbvralcsf  3767  sbcnestgf  4199  sbcco3g  4203  ralrnmpt  6593  tfindes  7295  findcard2  8442  ac6sfi  8446  indexfi  8516  nn1suc  11329  uzind4s2  11970  wrdind  13703  wrd2ind  13704  prmind2  15619  mrcmndind  17574  elmptrab  21848  isfildlem  21878  ifeqeqx  29692  bnj609  31315  bnj601  31318  sdclem2  33851  fdc1  33855  sbccom2  34242  sbccom2f  34243  sbccom2fi  34244  elimhyps  34742  dedths  34743  elimhyps2  34745  dedths2  34746  lshpkrlem3  34894  rexrabdioph  37861  rexfrabdioph  37862  2rexfrabdioph  37863  3rexfrabdioph  37864  4rexfrabdioph  37865  6rexfrabdioph  37866  7rexfrabdioph  37867  2nn0ind  38012  zindbi  38013  axfrege52c  38682  frege58c  38716  frege92  38750  2sbc6g  39116  2sbc5g  39117  pm14.122b  39124  pm14.24  39133  iotavalsb  39134  sbiota1  39135  fvsb  39155