Theorem dfsbcq 3719

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

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107  {cab 2716  [wsbc 3717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-sbc 3718

This theorem is referenced by:  sbceq1d  3722  sbc8g  3725  spsbc  3730  sbccow  3740  sbcco  3743  sbcco2  3744  sbcie2g  3759  elrabsf  3765  eqsbc1  3766  csbeq1  3836  cbvralcsf  3878  sbcnestgfw  4353  sbcco3gw  4357  sbcnestgf  4358  sbcco3g  4362  csbie2df  4375  reusngf  4609  reuprg0  4639  sbcop  5404  reuop  6200  ralrnmptw  6979  ralrnmpt  6981  tfindes  7718  findcard2  8956  findcard2OLD  9065  ac6sfi  9067  indexfi  9136  nn1suc  12004  uzind4s2  12658  wrdind  14444  wrd2ind  14445  prmind2  16399  mndind  18475  elmptrab  22987  isfildlem  23017  ifeqeqx  30894  wrdt2ind  31234  bnj609  32906  bnj601  32909  sdclem2  35909  fdc1  35913  sbccom2  36292  sbccom2f  36293  sbccom2fi  36294  elimhyps  36982  dedths  36983  elimhyps2  36985  dedths2  36986  lshpkrlem3  37133  rexrabdioph  40623  rexfrabdioph  40624  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  2nn0ind  40774  zindbi  40775  axfrege52c  41502  frege58c  41536  frege92  41570  2sbc6g  42040  2sbc5g  42041  pm14.122b  42048  pm14.24  42057  iotavalsb  42058  sbiota1  42059  fvsb  42077  or2expropbilem1  44537  ich2exprop  44934  reupr  44985