Theorem dfsbcq 3404

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

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  {cab 2596  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-sbc 3403

This theorem is referenced by:  sbceq1d  3407  sbc8g  3410  spsbc  3415  sbcco  3425  sbcco2  3426  sbcie2g  3436  elrabsf  3441  eqsbc3  3442  csbeq1  3502  cbvralcsf  3531  sbcnestgf  3947  sbcco3g  3951  ralrnmpt  6276  tfindes  6954  findcard2  8085  ac6sfi  8089  indexfi  8157  nn1suc  10918  uzind4s2  11625  wrdind  13328  wrd2ind  13329  prmind2  15236  mrcmndind  17189  elmptrab  21440  isfildlem  21471  ifeqeqx  28745  bnj609  30241  bnj601  30244  sdclem2  32708  fdc1  32712  sbccom2  33100  sbccom2f  33101  sbccom2fi  33102  elimhyps  33265  dedths  33266  elimhyps2  33268  dedths2  33269  lshpkrlem3  33417  rexrabdioph  36376  rexfrabdioph  36377  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  2nn0ind  36528  zindbi  36529  axfrege52c  37201  frege58c  37235  frege92  37269  2sbc6g  37638  2sbc5g  37639  pm14.122b  37646  pm14.24  37655  iotavalsb  37656  sbiota1  37657  fvsb  37677