Theorem dfsbcq 3744

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

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {cab 2741  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-sbc 3743

This theorem is used by:  sbceq1d  3747  sbc8g  3750  spsbc  3755  sbccow  3765  sbcco  3768  sbcco2  3769  sbcie2g  3782  elrabsf  3787  eqsbc1  3788  csbeq1  3854  cbvralcsf  3893  sbcnestgfw  4382  sbcco3gw  4386  sbcnestgf  4387  sbcco3g  4391  csbie2df  4404  reusngf  4635  reuprg0  4663  sbcop  5463  reuop  6314  ralrnmptw  7118  ralrnmpt  7120  tfindes  7898  findcard2  9208  ac6sfi  9303  indexfi  9377  nn1suc  12384  uzind4s2  13063  wrdind  14899  wrd2ind  14900  prmind2  16889  mndind  19053  elmptrab  24176  isfildlem  24206  ifeqeqx  33210  wrdt2ind  33586  bnj609  35617  bnj601  35620  weiunlem  37429  sdclem2  38868  fdc1  38872  sbccom2  39249  sbccom2f  39250  sbccom2fi  39251  elimhyps  40210  dedths  40211  elimhyps2  40213  dedths2  40214  lshpkrlem3  40361  rexrabdioph  43994  rexfrabdioph  43995  2rexfrabdioph  43996  3rexfrabdioph  43997  4rexfrabdioph  43998  6rexfrabdioph  43999  7rexfrabdioph  44000  2nn0ind  44145  zindbi  44146  axfrege52c  45079  frege58c  45113  frege92  45147  2sbc6g  45591  2sbc5g  45592  pm14.122b  45598  pm14.24  45607  iotavalsb  45608  sbiota1  45609  fvsb  45625  or2expropbilem1  48307  ich2exprop  48758  reupr  48809