Theorem dfsbcq 3779

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

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2709  [wsbc 3777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-sbc 3778

This theorem is referenced by:  sbceq1d  3782  sbc8g  3785  spsbc  3790  sbccow  3800  sbcco  3803  sbcco2  3804  sbcie2g  3819  elrabsf  3825  eqsbc1  3826  csbeq1  3896  cbvralcsf  3938  sbcnestgfw  4418  sbcco3gw  4422  sbcnestgf  4423  sbcco3g  4427  csbie2df  4440  reusngf  4676  reuprg0  4706  sbcop  5489  reuop  6292  ralrnmptw  7095  ralrnmpt  7097  tfindes  7851  findcard2  9163  findcard2OLD  9283  ac6sfi  9286  indexfi  9359  nn1suc  12233  uzind4s2  12892  wrdind  14671  wrd2ind  14672  prmind2  16621  mndind  18708  elmptrab  23330  isfildlem  23360  ifeqeqx  31769  wrdt2ind  32112  bnj609  33923  bnj601  33926  sdclem2  36605  fdc1  36609  sbccom2  36988  sbccom2f  36989  sbccom2fi  36990  elimhyps  37826  dedths  37827  elimhyps2  37829  dedths2  37830  lshpkrlem3  37977  rexrabdioph  41522  rexfrabdioph  41523  2rexfrabdioph  41524  3rexfrabdioph  41525  4rexfrabdioph  41526  6rexfrabdioph  41527  7rexfrabdioph  41528  2nn0ind  41674  zindbi  41675  axfrege52c  42628  frege58c  42662  frege92  42696  2sbc6g  43164  2sbc5g  43165  pm14.122b  43172  pm14.24  43181  iotavalsb  43182  sbiota1  43183  fvsb  43201  or2expropbilem1  45732  ich2exprop  46129  reupr  46180