Theorem dfsbcq 3713

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

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  {cab 2715  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  sbceq1d  3716  sbc8g  3719  spsbc  3724  sbccow  3734  sbcco  3737  sbcco2  3738  sbcie2g  3753  elrabsf  3759  eqsbc1  3760  csbeq1  3831  cbvralcsf  3873  sbcnestgfw  4349  sbcco3gw  4353  sbcnestgf  4354  sbcco3g  4358  csbie2df  4371  reusngf  4605  reuprg0  4635  sbcop  5397  reuop  6185  ralrnmptw  6952  ralrnmpt  6954  tfindes  7684  findcard2  8909  findcard2OLD  8986  ac6sfi  8988  indexfi  9057  nn1suc  11925  uzind4s2  12578  wrdind  14363  wrd2ind  14364  prmind2  16318  mndind  18381  elmptrab  22886  isfildlem  22916  ifeqeqx  30786  wrdt2ind  31127  bnj609  32797  bnj601  32800  sdclem2  35827  fdc1  35831  sbccom2  36210  sbccom2f  36211  sbccom2fi  36212  elimhyps  36902  dedths  36903  elimhyps2  36905  dedths2  36906  lshpkrlem3  37053  rexrabdioph  40532  rexfrabdioph  40533  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  2nn0ind  40683  zindbi  40684  axfrege52c  41384  frege58c  41418  frege92  41452  2sbc6g  41922  2sbc5g  41923  pm14.122b  41930  pm14.24  41939  iotavalsb  41940  sbiota1  41941  fvsb  41959  or2expropbilem1  44413  ich2exprop  44811  reupr  44862