Theorem dfsbcq 3740

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {cab 2711  [wsbc 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808  df-sbc 3739

This theorem is referenced by:  sbceq1d  3743  sbc8g  3746  spsbc  3751  sbccow  3761  sbcco  3764  sbcco2  3765  sbcie2g  3779  elrabsf  3784  eqsbc1  3785  csbeq1  3850  cbvralcsf  3889  sbcnestgfw  4372  sbcco3gw  4376  sbcnestgf  4377  sbcco3g  4381  csbie2df  4394  reusngf  4628  reuprg0  4656  sbcop  5434  reuop  6248  ralrnmptw  7036  ralrnmpt  7038  tfindes  7802  findcard2  9084  ac6sfi  9178  indexfi  9254  nn1suc  12157  uzind4s2  12817  wrdind  14639  wrd2ind  14640  prmind2  16606  mndind  18746  elmptrab  23752  isfildlem  23782  ifeqeqx  32533  wrdt2ind  32945  bnj609  34940  bnj601  34943  weiunlem2  36518  sdclem2  37792  fdc1  37796  sbccom2  38175  sbccom2f  38176  sbccom2fi  38177  elimhyps  39070  dedths  39071  elimhyps2  39073  dedths2  39074  lshpkrlem3  39221  rexrabdioph  42901  rexfrabdioph  42902  2rexfrabdioph  42903  3rexfrabdioph  42904  4rexfrabdioph  42905  6rexfrabdioph  42906  7rexfrabdioph  42907  2nn0ind  43052  zindbi  43053  axfrege52c  43994  frege58c  44028  frege92  44062  2sbc6g  44522  2sbc5g  44523  pm14.122b  44530  pm14.24  44539  iotavalsb  44540  sbiota1  44541  fvsb  44558  or2expropbilem1  47146  ich2exprop  47585  reupr  47636