Theorem dfsbcq 3741

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2110  {cab 2708  [wsbc 3739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-clel 2804  df-sbc 3740

This theorem is referenced by:  sbceq1d  3744  sbc8g  3747  spsbc  3752  sbccow  3762  sbcco  3765  sbcco2  3766  sbcie2g  3780  elrabsf  3785  eqsbc1  3786  csbeq1  3851  cbvralcsf  3890  sbcnestgfw  4369  sbcco3gw  4373  sbcnestgf  4374  sbcco3g  4378  csbie2df  4391  reusngf  4625  reuprg0  4653  sbcop  5427  reuop  6236  ralrnmptw  7022  ralrnmpt  7024  tfindes  7788  findcard2  9069  ac6sfi  9163  indexfi  9239  nn1suc  12139  uzind4s2  12799  wrdind  14621  wrd2ind  14622  prmind2  16588  mndind  18728  elmptrab  23735  isfildlem  23765  ifeqeqx  32512  wrdt2ind  32924  bnj609  34919  bnj601  34922  weiunlem2  36476  sdclem2  37761  fdc1  37765  sbccom2  38144  sbccom2f  38145  sbccom2fi  38146  elimhyps  38979  dedths  38980  elimhyps2  38982  dedths2  38983  lshpkrlem3  39130  rexrabdioph  42806  rexfrabdioph  42807  2rexfrabdioph  42808  3rexfrabdioph  42809  4rexfrabdioph  42810  6rexfrabdioph  42811  7rexfrabdioph  42812  2nn0ind  42957  zindbi  42958  axfrege52c  43899  frege58c  43933  frege92  43967  2sbc6g  44427  2sbc5g  44428  pm14.122b  44435  pm14.24  44444  iotavalsb  44445  sbiota1  44446  fvsb  44463  or2expropbilem1  47042  ich2exprop  47481  reupr  47532