Theorem dfsbcq 3732

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

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {cab 2718  [wsbc 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815  df-sbc 3731

This theorem is referenced by:  sbceq1d  3735  sbc8g  3738  spsbc  3743  sbccow  3753  sbcco  3756  sbcco2  3757  sbcie2g  3770  elrabsf  3775  eqsbc1  3776  csbeq1  3841  cbvralcsf  3880  sbcnestgfw  4356  sbcco3gw  4360  sbcnestgf  4361  sbcco3g  4365  csbie2df  4378  reusngf  4613  reuprg0  4641  sbcop  5436  reuop  6251  ralrnmptw  7042  ralrnmpt  7044  tfindes  7810  findcard2  9096  ac6sfi  9191  indexfi  9267  nn1suc  12194  uzind4s2  12857  wrdind  14682  wrd2ind  14683  prmind2  16652  mndind  18794  elmptrab  23817  isfildlem  23847  ifeqeqx  32637  wrdt2ind  33039  bnj609  35106  bnj601  35109  weiunlem  36692  sdclem2  38110  fdc1  38114  sbccom2  38493  sbccom2f  38494  sbccom2fi  38495  elimhyps  39454  dedths  39455  elimhyps2  39457  dedths2  39458  lshpkrlem3  39605  rexrabdioph  43240  rexfrabdioph  43241  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  2nn0ind  43391  zindbi  43392  axfrege52c  44332  frege58c  44366  frege92  44400  2sbc6g  44860  2sbc5g  44861  pm14.122b  44868  pm14.24  44877  iotavalsb  44878  sbiota1  44879  fvsb  44896  or2expropbilem1  47496  ich2exprop  47947  reupr  47998