Theorem dfsbcq 3758

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

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-sbc 3757

This theorem is referenced by:  sbceq1d  3761  sbc8g  3764  spsbc  3769  sbccow  3779  sbcco  3782  sbcco2  3783  sbcie2g  3797  elrabsf  3802  eqsbc1  3803  csbeq1  3868  cbvralcsf  3907  sbcnestgfw  4387  sbcco3gw  4391  sbcnestgf  4392  sbcco3g  4396  csbie2df  4409  reusngf  4641  reuprg0  4669  sbcop  5452  reuop  6269  ralrnmptw  7069  ralrnmpt  7071  tfindes  7842  findcard2  9134  ac6sfi  9238  indexfi  9318  nn1suc  12215  uzind4s2  12875  wrdind  14694  wrd2ind  14695  prmind2  16662  mndind  18762  elmptrab  23721  isfildlem  23751  ifeqeqx  32478  wrdt2ind  32882  bnj609  34914  bnj601  34917  weiunlem2  36458  sdclem2  37743  fdc1  37747  sbccom2  38126  sbccom2f  38127  sbccom2fi  38128  elimhyps  38961  dedths  38962  elimhyps2  38964  dedths2  38965  lshpkrlem3  39112  rexrabdioph  42789  rexfrabdioph  42790  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  2nn0ind  42941  zindbi  42942  axfrege52c  43883  frege58c  43917  frege92  43951  2sbc6g  44411  2sbc5g  44412  pm14.122b  44419  pm14.24  44428  iotavalsb  44429  sbiota1  44430  fvsb  44448  or2expropbilem1  47037  ich2exprop  47476  reupr  47527