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 2100 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 1570   ∈ wcel 2145  {cab 2738  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  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  5457  reuop  6285  ralrnmptw  7082  ralrnmpt  7084  tfindes  7857  findcard2  9158  ac6sfi  9253  indexfi  9327  nn1suc  12327  uzind4s2  13006  wrdind  14839  wrd2ind  14840  prmind2  16823  mndind  18986  elmptrab  24108  isfildlem  24138  ifeqeqx  33072  wrdt2ind  33450  bnj609  35482  bnj601  35485  weiunlem  37173  sdclem2  38596  fdc1  38600  sbccom2  38977  sbccom2f  38978  sbccom2fi  38979  elimhyps  39938  dedths  39939  elimhyps2  39941  dedths2  39942  lshpkrlem3  40089  rexrabdioph  43739  rexfrabdioph  43740  2rexfrabdioph  43741  3rexfrabdioph  43742  4rexfrabdioph  43743  6rexfrabdioph  43744  7rexfrabdioph  43745  2nn0ind  43890  zindbi  43891  axfrege52c  44831  frege58c  44865  frege92  44899  2sbc6g  45343  2sbc5g  45344  pm14.122b  45351  pm14.24  45360  iotavalsb  45361  sbiota1  45362  fvsb  45378  or2expropbilem1  48024  ich2exprop  48475  reupr  48526