Theorem dfsbcq 3743

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  [wsbc 3741

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-sbc 3742

This theorem is referenced by:  sbceq1d  3746  sbc8g  3749  spsbc  3754  sbccow  3764  sbcco  3767  sbcco2  3768  sbcie2g  3782  elrabsf  3787  eqsbc1  3788  csbeq1  3853  cbvralcsf  3892  sbcnestgfw  4374  sbcco3gw  4378  sbcnestgf  4379  sbcco3g  4383  csbie2df  4396  reusngf  4632  reuprg0  4660  sbcop  5438  reuop  6252  ralrnmptw  7041  ralrnmpt  7043  tfindes  7807  findcard2  9093  ac6sfi  9188  indexfi  9264  nn1suc  12171  uzind4s2  12826  wrdind  14649  wrd2ind  14650  prmind2  16616  mndind  18757  elmptrab  23775  isfildlem  23805  ifeqeqx  32599  wrdt2ind  33016  bnj609  35054  bnj601  35057  weiunlem2  36638  sdclem2  37914  fdc1  37918  sbccom2  38297  sbccom2f  38298  sbccom2fi  38299  elimhyps  39258  dedths  39259  elimhyps2  39261  dedths2  39262  lshpkrlem3  39409  rexrabdioph  43072  rexfrabdioph  43073  2rexfrabdioph  43074  3rexfrabdioph  43075  4rexfrabdioph  43076  6rexfrabdioph  43077  7rexfrabdioph  43078  2nn0ind  43223  zindbi  43224  axfrege52c  44164  frege58c  44198  frege92  44232  2sbc6g  44692  2sbc5g  44693  pm14.122b  44700  pm14.24  44709  iotavalsb  44710  sbiota1  44711  fvsb  44728  or2expropbilem1  47314  ich2exprop  47753  reupr  47804