Theorem dfsbcq 3749

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

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {cab 2744  [wsbc 3747

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841  df-sbc 3748

This theorem is used by:  sbceq1d  3752  sbc8g  3755  spsbc  3760  sbccow  3770  sbcco  3773  sbcco2  3774  sbcie2g  3787  elrabsf  3792  eqsbc1  3793  csbeq1  3859  cbvralcsf  3898  sbcnestgfw  4389  sbcco3gw  4393  sbcnestgf  4394  sbcco3g  4398  csbie2df  4411  reusngf  4645  reuprg0  4673  sbcop  5476  reuop  6301  ralrnmptw  7096  ralrnmpt  7098  tfindes  7868  findcard2  9159  ac6sfi  9254  indexfi  9327  nn1suc  12273  uzind4s2  12951  wrdind  14783  wrd2ind  14784  prmind2  16768  mndind  18912  elmptrab  24014  isfildlem  24044  ifeqeqx  32918  wrdt2ind  33299  bnj609  35329  bnj601  35332  weiunlem  37007  sdclem2  38426  fdc1  38430  sbccom2  38807  sbccom2f  38808  sbccom2fi  38809  elimhyps  39768  dedths  39769  elimhyps2  39771  dedths2  39772  lshpkrlem3  39919  rexrabdioph  43554  rexfrabdioph  43555  2rexfrabdioph  43556  3rexfrabdioph  43557  4rexfrabdioph  43558  6rexfrabdioph  43559  7rexfrabdioph  43560  2nn0ind  43705  zindbi  43706  axfrege52c  44646  frege58c  44680  frege92  44714  2sbc6g  45158  2sbc5g  45159  pm14.122b  45166  pm14.24  45175  iotavalsb  45176  sbiota1  45177  fvsb  45193  or2expropbilem1  47802  ich2exprop  48253  reupr  48304