Theorem dfsbcq 3778

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

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  {cab 2703  [wsbc 3776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803  df-sbc 3777

This theorem is referenced by:  sbceq1d  3781  sbc8g  3784  spsbc  3789  sbccow  3799  sbcco  3802  sbcco2  3803  sbcie2g  3819  elrabsf  3825  eqsbc1  3826  csbeq1  3895  cbvralcsf  3937  sbcnestgfw  4423  sbcco3gw  4427  sbcnestgf  4428  sbcco3g  4432  csbie2df  4445  reusngf  4681  reuprg0  4711  sbcop  5495  reuop  6304  ralrnmptw  7108  ralrnmpt  7110  tfindes  7873  findcard2  9202  findcard2OLD  9318  ac6sfi  9321  indexfi  9404  nn1suc  12286  uzind4s2  12945  wrdind  14730  wrd2ind  14731  prmind2  16686  mndind  18818  elmptrab  23822  isfildlem  23852  ifeqeqx  32463  wrdt2ind  32817  bnj609  34762  bnj601  34765  sdclem2  37443  fdc1  37447  sbccom2  37826  sbccom2f  37827  sbccom2fi  37828  elimhyps  38659  dedths  38660  elimhyps2  38662  dedths2  38663  lshpkrlem3  38810  rexrabdioph  42451  rexfrabdioph  42452  2rexfrabdioph  42453  3rexfrabdioph  42454  4rexfrabdioph  42455  6rexfrabdioph  42456  7rexfrabdioph  42457  2nn0ind  42603  zindbi  42604  axfrege52c  43554  frege58c  43588  frege92  43622  2sbc6g  44089  2sbc5g  44090  pm14.122b  44097  pm14.24  44106  iotavalsb  44107  sbiota1  44108  fvsb  44126  or2expropbilem1  46647  ich2exprop  47043  reupr  47094