Theorem dfsbcq 3437

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

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  {cab 2608  [wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  sbceq1d  3440  sbc8g  3443  spsbc  3448  sbcco  3458  sbcco2  3459  sbcie2g  3469  elrabsf  3474  eqsbc3  3475  csbeq1  3536  cbvralcsf  3565  sbcnestgf  3995  sbcco3g  3999  ralrnmpt  6368  tfindes  7062  findcard2  8200  ac6sfi  8204  indexfi  8274  nn1suc  11041  uzind4s2  11749  wrdind  13476  wrd2ind  13477  prmind2  15398  mrcmndind  17366  elmptrab  21630  isfildlem  21661  ifeqeqx  29361  bnj609  30987  bnj601  30990  sdclem2  33538  fdc1  33542  sbccom2  33930  sbccom2f  33931  sbccom2fi  33932  elimhyps  34247  dedths  34248  elimhyps2  34250  dedths2  34251  lshpkrlem3  34399  rexrabdioph  37358  rexfrabdioph  37359  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  2nn0ind  37510  zindbi  37511  axfrege52c  38181  frege58c  38215  frege92  38249  2sbc6g  38616  2sbc5g  38617  pm14.122b  38624  pm14.24  38633  iotavalsb  38634  sbiota1  38635  fvsb  38656