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 2100 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 2850	. 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 2145  {cab 2740  [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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  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  3853  cbvralcsf  3892  sbcnestgfw  4382  sbcco3gw  4386  sbcnestgf  4387  sbcco3g  4391  csbie2df  4404  reusngf  4638  reuprg0  4666  sbcop  5469  reuop  6295  ralrnmptw  7091  ralrnmpt  7093  tfindes  7863  findcard2  9163  ac6sfi  9258  indexfi  9331  nn1suc  12283  uzind4s2  12962  wrdind  14795  wrd2ind  14796  prmind2  16781  mndind  18943  elmptrab  24059  isfildlem  24089  ifeqeqx  33025  wrdt2ind  33403  bnj609  35434  bnj601  35437  weiunlem  37090  sdclem2  38500  fdc1  38504  sbccom2  38881  sbccom2f  38882  sbccom2fi  38883  elimhyps  39842  dedths  39843  elimhyps2  39845  dedths2  39846  lshpkrlem3  39993  rexrabdioph  43643  rexfrabdioph  43644  2rexfrabdioph  43645  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  2nn0ind  43794  zindbi  43795  axfrege52c  44735  frege58c  44769  frege92  44803  2sbc6g  45247  2sbc5g  45248  pm14.122b  45255  pm14.24  45264  iotavalsb  45265  sbiota1  45266  fvsb  45282  or2expropbilem1  47928  ich2exprop  48379  reupr  48430