Theorem dfsbcq 3708

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

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522   ∈ wcel 2081  {cab 2775  [wsbc 3706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863  df-sbc 3707

This theorem is referenced by:  sbceq1d  3711  sbc8g  3714  spsbc  3719  sbcco  3729  sbcco2  3730  sbcie2g  3740  elrabsf  3745  eqsbc3  3746  eqsbc3OLD  3747  csbeq1  3814  cbvralcsf  3849  sbcnestgf  4290  sbcco3g  4294  reusngf  4519  reuprg0  4545  sbcop  5272  reuop  6019  ralrnmpt  6725  tfindes  7433  findcard2  8604  ac6sfi  8608  indexfi  8678  nn1suc  11507  uzind4s2  12158  wrdind  13920  wrd2ind  13921  prmind2  15858  mndind  17805  elmptrab  22119  isfildlem  22149  ifeqeqx  29986  wrdt2ind  30306  bnj609  31805  bnj601  31808  sdclem2  34549  fdc1  34553  sbccom2  34935  sbccom2f  34936  sbccom2fi  34937  elimhyps  35628  dedths  35629  elimhyps2  35631  dedths2  35632  lshpkrlem3  35779  rexrabdioph  38876  rexfrabdioph  38877  2rexfrabdioph  38878  3rexfrabdioph  38879  4rexfrabdioph  38880  6rexfrabdioph  38881  7rexfrabdioph  38882  2nn0ind  39027  zindbi  39028  axfrege52c  39718  frege58c  39752  frege92  39786  2sbc6g  40285  2sbc5g  40286  pm14.122b  40293  pm14.24  40302  iotavalsb  40303  sbiota1  40304  fvsb  40323  or2expropbilem1  42783  ich2exprop  43115  reupr  43166