Theorem dfsbcq 3755

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-sbc 3754

This theorem is referenced by:  sbceq1d  3758  sbc8g  3761  spsbc  3766  sbccow  3776  sbcco  3779  sbcco2  3780  sbcie2g  3794  elrabsf  3799  eqsbc1  3800  csbeq1  3865  cbvralcsf  3904  sbcnestgfw  4384  sbcco3gw  4388  sbcnestgf  4389  sbcco3g  4393  csbie2df  4406  reusngf  4638  reuprg0  4666  sbcop  5449  reuop  6266  ralrnmptw  7066  ralrnmpt  7068  tfindes  7839  findcard2  9128  ac6sfi  9231  indexfi  9311  nn1suc  12208  uzind4s2  12868  wrdind  14687  wrd2ind  14688  prmind2  16655  mndind  18755  elmptrab  23714  isfildlem  23744  ifeqeqx  32471  wrdt2ind  32875  bnj609  34907  bnj601  34910  weiunlem2  36451  sdclem2  37736  fdc1  37740  sbccom2  38119  sbccom2f  38120  sbccom2fi  38121  elimhyps  38954  dedths  38955  elimhyps2  38957  dedths2  38958  lshpkrlem3  39105  rexrabdioph  42782  rexfrabdioph  42783  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  2nn0ind  42934  zindbi  42935  axfrege52c  43876  frege58c  43910  frege92  43944  2sbc6g  44404  2sbc5g  44405  pm14.122b  44412  pm14.24  44421  iotavalsb  44422  sbiota1  44423  fvsb  44441  or2expropbilem1  47033  ich2exprop  47472  reupr  47523