Theorem dfsbcq 3696

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

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2110  {cab 2714  [wsbc 3694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729  df-clel 2816  df-sbc 3695

This theorem is referenced by:  sbceq1d  3699  sbc8g  3702  spsbc  3707  sbccow  3717  sbcco  3720  sbcco2  3721  sbcie2g  3736  elrabsf  3742  eqsbc3  3743  csbeq1  3814  cbvralcsf  3856  sbcnestgfw  4333  sbcco3gw  4337  sbcnestgf  4338  sbcco3g  4342  csbie2df  4355  reusngf  4588  reuprg0  4618  sbcop  5372  reuop  6156  ralrnmptw  6913  ralrnmpt  6915  tfindes  7641  findcard2  8842  findcard2OLD  8913  ac6sfi  8915  indexfi  8984  nn1suc  11852  uzind4s2  12505  wrdind  14287  wrd2ind  14288  prmind2  16242  mndind  18254  elmptrab  22724  isfildlem  22754  ifeqeqx  30604  wrdt2ind  30945  bnj609  32610  bnj601  32613  sdclem2  35637  fdc1  35641  sbccom2  36020  sbccom2f  36021  sbccom2fi  36022  elimhyps  36712  dedths  36713  elimhyps2  36715  dedths2  36716  lshpkrlem3  36863  rexrabdioph  40319  rexfrabdioph  40320  2rexfrabdioph  40321  3rexfrabdioph  40322  4rexfrabdioph  40323  6rexfrabdioph  40324  7rexfrabdioph  40325  2nn0ind  40470  zindbi  40471  axfrege52c  41172  frege58c  41206  frege92  41240  2sbc6g  41706  2sbc5g  41707  pm14.122b  41714  pm14.24  41723  iotavalsb  41724  sbiota1  41725  fvsb  41743  or2expropbilem1  44198  ich2exprop  44596  reupr  44647