Theorem dfsbcq 3789

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  {cab 2713  [wsbc 3787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-clel 2815  df-sbc 3788

This theorem is referenced by:  sbceq1d  3792  sbc8g  3795  spsbc  3800  sbccow  3810  sbcco  3813  sbcco2  3814  sbcie2g  3828  elrabsf  3833  eqsbc1  3834  csbeq1  3901  cbvralcsf  3940  sbcnestgfw  4420  sbcco3gw  4424  sbcnestgf  4425  sbcco3g  4429  csbie2df  4442  reusngf  4673  reuprg0  4701  sbcop  5493  reuop  6312  ralrnmptw  7113  ralrnmpt  7115  tfindes  7885  findcard2  9205  ac6sfi  9321  indexfi  9401  nn1suc  12289  uzind4s2  12952  wrdind  14761  wrd2ind  14762  prmind2  16723  mndind  18842  elmptrab  23836  isfildlem  23866  ifeqeqx  32556  wrdt2ind  32939  bnj609  34932  bnj601  34935  weiunlem2  36465  sdclem2  37750  fdc1  37754  sbccom2  38133  sbccom2f  38134  sbccom2fi  38135  elimhyps  38963  dedths  38964  elimhyps2  38966  dedths2  38967  lshpkrlem3  39114  rexrabdioph  42810  rexfrabdioph  42811  2rexfrabdioph  42812  3rexfrabdioph  42813  4rexfrabdioph  42814  6rexfrabdioph  42815  7rexfrabdioph  42816  2nn0ind  42962  zindbi  42963  axfrege52c  43905  frege58c  43939  frege92  43973  2sbc6g  44439  2sbc5g  44440  pm14.122b  44447  pm14.24  44456  iotavalsb  44457  sbiota1  44458  fvsb  44476  or2expropbilem1  47049  ich2exprop  47463  reupr  47514