Theorem dfsbcq 3746

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

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-sbc 3745

This theorem is referenced by:  sbceq1d  3749  sbc8g  3752  spsbc  3757  sbccow  3767  sbcco  3770  sbcco2  3771  sbcie2g  3785  elrabsf  3790  eqsbc1  3791  csbeq1  3856  cbvralcsf  3895  sbcnestgfw  4374  sbcco3gw  4378  sbcnestgf  4379  sbcco3g  4383  csbie2df  4396  reusngf  4628  reuprg0  4656  sbcop  5436  reuop  6245  ralrnmptw  7032  ralrnmpt  7034  tfindes  7803  findcard2  9088  ac6sfi  9189  indexfi  9269  nn1suc  12168  uzind4s2  12828  wrdind  14646  wrd2ind  14647  prmind2  16614  mndind  18720  elmptrab  23730  isfildlem  23760  ifeqeqx  32504  wrdt2ind  32908  bnj609  34883  bnj601  34886  weiunlem2  36436  sdclem2  37721  fdc1  37725  sbccom2  38104  sbccom2f  38105  sbccom2fi  38106  elimhyps  38939  dedths  38940  elimhyps2  38942  dedths2  38943  lshpkrlem3  39090  rexrabdioph  42767  rexfrabdioph  42768  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  2nn0ind  42918  zindbi  42919  axfrege52c  43860  frege58c  43894  frege92  43928  2sbc6g  44388  2sbc5g  44389  pm14.122b  44396  pm14.24  44405  iotavalsb  44406  sbiota1  44407  fvsb  44425  or2expropbilem1  47017  ich2exprop  47456  reupr  47507