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 2061 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 2816	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}))
2		df-sbc 3775	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		df-sbc 3775	. 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})
4	1, 2, 3	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  {cab 2704  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-clel 2805  df-sbc 3775

This theorem is referenced by:  sbceq1d  3779  sbc8g  3782  spsbc  3787  sbccow  3797  sbcco  3800  sbcco2  3801  sbcie2g  3816  elrabsf  3822  eqsbc1  3823  csbeq1  3892  cbvralcsf  3934  sbcnestgfw  4414  sbcco3gw  4418  sbcnestgf  4419  sbcco3g  4423  csbie2df  4436  reusngf  4672  reuprg0  4702  sbcop  5485  reuop  6291  ralrnmptw  7098  ralrnmpt  7100  tfindes  7861  findcard2  9180  findcard2OLD  9300  ac6sfi  9303  indexfi  9376  nn1suc  12256  uzind4s2  12915  wrdind  14696  wrd2ind  14697  prmind2  16647  mndind  18771  elmptrab  23718  isfildlem  23748  ifeqeqx  32318  wrdt2ind  32656  bnj609  34484  bnj601  34487  sdclem2  37150  fdc1  37154  sbccom2  37533  sbccom2f  37534  sbccom2fi  37535  elimhyps  38370  dedths  38371  elimhyps2  38373  dedths2  38374  lshpkrlem3  38521  rexrabdioph  42136  rexfrabdioph  42137  2rexfrabdioph  42138  3rexfrabdioph  42139  4rexfrabdioph  42140  6rexfrabdioph  42141  7rexfrabdioph  42142  2nn0ind  42288  zindbi  42289  axfrege52c  43240  frege58c  43274  frege92  43308  2sbc6g  43775  2sbc5g  43776  pm14.122b  43783  pm14.24  43792  iotavalsb  43793  sbiota1  43794  fvsb  43812  or2expropbilem1  46337  ich2exprop  46734  reupr  46785