Theorem dfsbcq 3776

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

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {cab 2702  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802  df-sbc 3775

This theorem is referenced by:  sbceq1d  3779  sbc8g  3782  spsbc  3787  sbccow  3797  sbcco  3800  sbcco2  3801  sbcie2g  3817  elrabsf  3823  eqsbc1  3824  csbeq1  3893  cbvralcsf  3935  sbcnestgfw  4419  sbcco3gw  4423  sbcnestgf  4424  sbcco3g  4428  csbie2df  4441  reusngf  4677  reuprg0  4707  sbcop  5490  reuop  6297  ralrnmptw  7101  ralrnmpt  7103  tfindes  7866  findcard2  9187  findcard2OLD  9307  ac6sfi  9310  indexfi  9384  nn1suc  12264  uzind4s2  12923  wrdind  14704  wrd2ind  14705  prmind2  16655  mndind  18784  elmptrab  23761  isfildlem  23791  ifeqeqx  32390  wrdt2ind  32731  bnj609  34618  bnj601  34621  sdclem2  37285  fdc1  37289  sbccom2  37668  sbccom2f  37669  sbccom2fi  37670  elimhyps  38502  dedths  38503  elimhyps2  38505  dedths2  38506  lshpkrlem3  38653  rexrabdioph  42279  rexfrabdioph  42280  2rexfrabdioph  42281  3rexfrabdioph  42282  4rexfrabdioph  42283  6rexfrabdioph  42284  7rexfrabdioph  42285  2nn0ind  42431  zindbi  42432  axfrege52c  43382  frege58c  43416  frege92  43450  2sbc6g  43917  2sbc5g  43918  pm14.122b  43925  pm14.24  43934  iotavalsb  43935  sbiota1  43936  fvsb  43954  or2expropbilem1  46477  ich2exprop  46874  reupr  46925