Theorem dfsbcq 3738

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {cab 2709  [wsbc 3736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-sbc 3737

This theorem is referenced by:  sbceq1d  3741  sbc8g  3744  spsbc  3749  sbccow  3759  sbcco  3762  sbcco2  3763  sbcie2g  3777  elrabsf  3782  eqsbc1  3783  csbeq1  3848  cbvralcsf  3887  sbcnestgfw  4368  sbcco3gw  4372  sbcnestgf  4373  sbcco3g  4377  csbie2df  4390  reusngf  4624  reuprg0  4652  sbcop  5427  reuop  6240  ralrnmptw  7027  ralrnmpt  7029  tfindes  7793  findcard2  9074  ac6sfi  9168  indexfi  9244  nn1suc  12147  uzind4s2  12807  wrdind  14629  wrd2ind  14630  prmind2  16596  mndind  18736  elmptrab  23742  isfildlem  23772  ifeqeqx  32522  wrdt2ind  32934  bnj609  34929  bnj601  34932  weiunlem2  36507  sdclem2  37781  fdc1  37785  sbccom2  38164  sbccom2f  38165  sbccom2fi  38166  elimhyps  39059  dedths  39060  elimhyps2  39062  dedths2  39063  lshpkrlem3  39210  rexrabdioph  42886  rexfrabdioph  42887  2rexfrabdioph  42888  3rexfrabdioph  42889  4rexfrabdioph  42890  6rexfrabdioph  42891  7rexfrabdioph  42892  2nn0ind  43037  zindbi  43038  axfrege52c  43979  frege58c  44013  frege92  44047  2sbc6g  44507  2sbc5g  44508  pm14.122b  44515  pm14.24  44524  iotavalsb  44525  sbiota1  44526  fvsb  44543  or2expropbilem1  47131  ich2exprop  47570  reupr  47621