Theorem dfsbcq 3740

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

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {cab 2738  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  sbceq1d  3743  sbc8g  3746  spsbc  3751  sbccow  3761  sbcco  3764  sbcco2  3765  sbcie2g  3778  elrabsf  3783  eqsbc1  3784  csbeq1  3849  cbvralcsf  3888  sbcnestgfw  4378  sbcco3gw  4382  sbcnestgf  4383  sbcco3g  4387  csbie2df  4400  reusngf  4634  reuprg0  4662  sbcop  5458  reuop  6296  ralrnmptw  7094  ralrnmpt  7096  tfindes  7874  findcard2  9181  ac6sfi  9276  indexfi  9350  nn1suc  12358  uzind4s2  13037  wrdind  14872  wrd2ind  14873  prmind2  16861  mndind  19025  elmptrab  24147  isfildlem  24177  ifeqeqx  33181  wrdt2ind  33559  bnj609  35590  bnj601  35593  weiunlem  37326  sdclem2  38752  fdc1  38756  sbccom2  39133  sbccom2f  39134  sbccom2fi  39135  elimhyps  40094  dedths  40095  elimhyps2  40097  dedths2  40098  lshpkrlem3  40245  rexrabdioph  43877  rexfrabdioph  43878  2rexfrabdioph  43879  3rexfrabdioph  43880  4rexfrabdioph  43881  6rexfrabdioph  43882  7rexfrabdioph  43883  2nn0ind  44028  zindbi  44029  axfrege52c  44963  frege58c  44997  frege92  45031  2sbc6g  45475  2sbc5g  45476  pm14.122b  45483  pm14.24  45492  iotavalsb  45493  sbiota1  45494  fvsb  45510  or2expropbilem1  48178  ich2exprop  48629  reupr  48680