Theorem dfsbcq 3806

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {cab 2717  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  sbceq1d  3809  sbc8g  3812  spsbc  3817  sbccow  3827  sbcco  3830  sbcco2  3831  sbcie2g  3847  elrabsf  3853  eqsbc1  3854  csbeq1  3924  cbvralcsf  3966  sbcnestgfw  4444  sbcco3gw  4448  sbcnestgf  4449  sbcco3g  4453  csbie2df  4466  reusngf  4696  reuprg0  4727  sbcop  5509  reuop  6324  ralrnmptw  7128  ralrnmpt  7130  tfindes  7900  findcard2  9230  ac6sfi  9348  indexfi  9430  nn1suc  12315  uzind4s2  12974  wrdind  14770  wrd2ind  14771  prmind2  16732  mndind  18863  elmptrab  23856  isfildlem  23886  ifeqeqx  32565  wrdt2ind  32920  bnj609  34893  bnj601  34896  weiunlem2  36429  sdclem2  37702  fdc1  37706  sbccom2  38085  sbccom2f  38086  sbccom2fi  38087  elimhyps  38917  dedths  38918  elimhyps2  38920  dedths2  38921  lshpkrlem3  39068  rexrabdioph  42750  rexfrabdioph  42751  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  2nn0ind  42902  zindbi  42903  axfrege52c  43849  frege58c  43883  frege92  43917  2sbc6g  44384  2sbc5g  44385  pm14.122b  44392  pm14.24  44401  iotavalsb  44402  sbiota1  44403  fvsb  44421  or2expropbilem1  46947  ich2exprop  47345  reupr  47396