Theorem dfsbcq 3774

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

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  {cab 2799  [wsbc 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-sbc 3773

This theorem is referenced by:  sbceq1d  3777  sbc8g  3780  spsbc  3785  sbccow  3795  sbcco  3798  sbcco2  3799  sbcie2g  3811  elrabsf  3816  eqsbc3  3817  eqsbc3OLD  3818  csbeq1  3886  cbvralcsf  3925  sbcnestgfw  4370  sbcco3gw  4374  sbcnestgf  4375  sbcco3g  4379  csbie2df  4392  reusngf  4606  reuprg0  4632  sbcop  5373  reuop  6139  ralrnmptw  6855  ralrnmpt  6857  tfindes  7571  findcard2  8752  ac6sfi  8756  indexfi  8826  nn1suc  11653  uzind4s2  12303  wrdind  14078  wrd2ind  14079  prmind2  16023  mndind  17986  elmptrab  22429  isfildlem  22459  ifeqeqx  30291  wrdt2ind  30622  bnj609  32184  bnj601  32187  sdclem2  35011  fdc1  35015  sbccom2  35397  sbccom2f  35398  sbccom2fi  35399  elimhyps  36091  dedths  36092  elimhyps2  36094  dedths2  36095  lshpkrlem3  36242  rexrabdioph  39384  rexfrabdioph  39385  2rexfrabdioph  39386  3rexfrabdioph  39387  4rexfrabdioph  39388  6rexfrabdioph  39389  7rexfrabdioph  39390  2nn0ind  39535  zindbi  39536  axfrege52c  40226  frege58c  40260  frege92  40294  2sbc6g  40740  2sbc5g  40741  pm14.122b  40748  pm14.24  40757  iotavalsb  40758  sbiota1  40759  fvsb  40777  or2expropbilem1  43260  ich2exprop  43626  reupr  43677