Theorem dfsbcq 3745

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

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  {cab 2739  [wsbc 3743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753  df-clel 2836  df-sbc 3744

This theorem is referenced by:  sbceq1d  3748  sbc8g  3751  spsbc  3756  sbccow  3766  sbcco  3769  sbcco2  3770  sbcie2g  3783  elrabsf  3788  eqsbc1  3789  csbeq1  3855  cbvralcsf  3894  sbcnestgfw  4385  sbcco3gw  4389  sbcnestgf  4390  sbcco3g  4394  csbie2df  4407  reusngf  4639  reuprg0  4667  sbcop  5471  reuop  6294  ralrnmptw  7089  ralrnmpt  7091  tfindes  7858  findcard2  9148  ac6sfi  9243  indexfi  9316  nn1suc  12254  uzind4s2  12932  wrdind  14759  wrd2ind  14760  prmind2  16742  mndind  18886  elmptrab  23963  isfildlem  23993  ifeqeqx  32854  wrdt2ind  33239  bnj609  35271  bnj601  35274  weiunlem  36940  sdclem2  38359  fdc1  38363  sbccom2  38742  sbccom2f  38743  sbccom2fi  38744  elimhyps  39703  dedths  39704  elimhyps2  39706  dedths2  39707  lshpkrlem3  39854  rexrabdioph  43491  rexfrabdioph  43492  2rexfrabdioph  43493  3rexfrabdioph  43494  4rexfrabdioph  43495  6rexfrabdioph  43496  7rexfrabdioph  43497  2nn0ind  43642  zindbi  43643  axfrege52c  44583  frege58c  44617  frege92  44651  2sbc6g  45095  2sbc5g  45096  pm14.122b  45103  pm14.24  45112  iotavalsb  45113  sbiota1  45114  fvsb  45130  or2expropbilem1  47736  ich2exprop  48187  reupr  48238