Theorem dfsbcq 3772

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2714  [wsbc 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810  df-sbc 3771

This theorem is referenced by:  sbceq1d  3775  sbc8g  3778  spsbc  3783  sbccow  3793  sbcco  3796  sbcco2  3797  sbcie2g  3811  elrabsf  3816  eqsbc1  3817  csbeq1  3882  cbvralcsf  3921  sbcnestgfw  4401  sbcco3gw  4405  sbcnestgf  4406  sbcco3g  4410  csbie2df  4423  reusngf  4655  reuprg0  4683  sbcop  5469  reuop  6287  ralrnmptw  7089  ralrnmpt  7091  tfindes  7863  findcard2  9183  ac6sfi  9297  indexfi  9377  nn1suc  12267  uzind4s2  12930  wrdind  14745  wrd2ind  14746  prmind2  16709  mndind  18811  elmptrab  23770  isfildlem  23800  ifeqeqx  32528  wrdt2ind  32934  bnj609  34953  bnj601  34956  weiunlem2  36486  sdclem2  37771  fdc1  37775  sbccom2  38154  sbccom2f  38155  sbccom2fi  38156  elimhyps  38984  dedths  38985  elimhyps2  38987  dedths2  38988  lshpkrlem3  39135  rexrabdioph  42792  rexfrabdioph  42793  2rexfrabdioph  42794  3rexfrabdioph  42795  4rexfrabdioph  42796  6rexfrabdioph  42797  7rexfrabdioph  42798  2nn0ind  42944  zindbi  42945  axfrege52c  43886  frege58c  43920  frege92  43954  2sbc6g  44414  2sbc5g  44415  pm14.122b  44422  pm14.24  44431  iotavalsb  44432  sbiota1  44433  fvsb  44451  or2expropbilem1  47041  ich2exprop  47465  reupr  47516