Theorem dfsbcq 3793

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {cab 2712  [wsbc 3791

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814  df-sbc 3792

This theorem is referenced by:  sbceq1d  3796  sbc8g  3799  spsbc  3804  sbccow  3814  sbcco  3817  sbcco2  3818  sbcie2g  3834  elrabsf  3840  eqsbc1  3841  csbeq1  3911  cbvralcsf  3953  sbcnestgfw  4427  sbcco3gw  4431  sbcnestgf  4432  sbcco3g  4436  csbie2df  4449  reusngf  4679  reuprg0  4707  sbcop  5500  reuop  6315  ralrnmptw  7114  ralrnmpt  7116  tfindes  7884  findcard2  9203  ac6sfi  9318  indexfi  9398  nn1suc  12286  uzind4s2  12949  wrdind  14757  wrd2ind  14758  prmind2  16719  mndind  18854  elmptrab  23851  isfildlem  23881  ifeqeqx  32563  wrdt2ind  32923  bnj609  34910  bnj601  34913  weiunlem2  36446  sdclem2  37729  fdc1  37733  sbccom2  38112  sbccom2f  38113  sbccom2fi  38114  elimhyps  38943  dedths  38944  elimhyps2  38946  dedths2  38947  lshpkrlem3  39094  rexrabdioph  42782  rexfrabdioph  42783  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  2nn0ind  42934  zindbi  42935  axfrege52c  43877  frege58c  43911  frege92  43945  2sbc6g  44411  2sbc5g  44412  pm14.122b  44419  pm14.24  44428  iotavalsb  44429  sbiota1  44430  fvsb  44448  or2expropbilem1  46982  ich2exprop  47396  reupr  47447