Theorem dfsbcq 3731

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

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  [wsbc 3729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-sbc 3730

This theorem is referenced by:  sbceq1d  3734  sbc8g  3737  spsbc  3742  sbccow  3752  sbcco  3755  sbcco2  3756  sbcie2g  3770  elrabsf  3775  eqsbc1  3776  csbeq1  3841  cbvralcsf  3880  sbcnestgfw  4362  sbcco3gw  4366  sbcnestgf  4367  sbcco3g  4371  csbie2df  4384  reusngf  4619  reuprg0  4647  sbcop  5443  reuop  6258  ralrnmptw  7047  ralrnmpt  7049  tfindes  7814  findcard2  9099  ac6sfi  9194  indexfi  9270  nn1suc  12196  uzind4s2  12859  wrdind  14684  wrd2ind  14685  prmind2  16654  mndind  18796  elmptrab  23792  isfildlem  23822  ifeqeqx  32612  wrdt2ind  33013  bnj609  35059  bnj601  35062  weiunlem  36645  sdclem2  38063  fdc1  38067  sbccom2  38446  sbccom2f  38447  sbccom2fi  38448  elimhyps  39407  dedths  39408  elimhyps2  39410  dedths2  39411  lshpkrlem3  39558  rexrabdioph  43222  rexfrabdioph  43223  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  2nn0ind  43373  zindbi  43374  axfrege52c  44314  frege58c  44348  frege92  44382  2sbc6g  44842  2sbc5g  44843  pm14.122b  44850  pm14.24  44859  iotavalsb  44860  sbiota1  44861  fvsb  44878  or2expropbilem1  47474  ich2exprop  47925  reupr  47976