Theorem dfsbcq 3780

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

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {cab 2707  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808  df-sbc 3779

This theorem is referenced by:  sbceq1d  3783  sbc8g  3786  spsbc  3791  sbccow  3801  sbcco  3804  sbcco2  3805  sbcie2g  3820  elrabsf  3826  eqsbc1  3827  csbeq1  3897  cbvralcsf  3939  sbcnestgfw  4419  sbcco3gw  4423  sbcnestgf  4424  sbcco3g  4428  csbie2df  4441  reusngf  4677  reuprg0  4707  sbcop  5490  reuop  6293  ralrnmptw  7096  ralrnmpt  7098  tfindes  7856  findcard2  9168  findcard2OLD  9288  ac6sfi  9291  indexfi  9364  nn1suc  12240  uzind4s2  12899  wrdind  14678  wrd2ind  14679  prmind2  16628  mndind  18747  elmptrab  23553  isfildlem  23583  ifeqeqx  32039  wrdt2ind  32382  bnj609  34224  bnj601  34227  sdclem2  36915  fdc1  36919  sbccom2  37298  sbccom2f  37299  sbccom2fi  37300  elimhyps  38136  dedths  38137  elimhyps2  38139  dedths2  38140  lshpkrlem3  38287  rexrabdioph  41836  rexfrabdioph  41837  2rexfrabdioph  41838  3rexfrabdioph  41839  4rexfrabdioph  41840  6rexfrabdioph  41841  7rexfrabdioph  41842  2nn0ind  41988  zindbi  41989  axfrege52c  42942  frege58c  42976  frege92  43010  2sbc6g  43478  2sbc5g  43479  pm14.122b  43486  pm14.24  43495  iotavalsb  43496  sbiota1  43497  fvsb  43515  or2expropbilem1  46042  ich2exprop  46439  reupr  46490