Theorem dfsbcq 3744

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

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

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

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 3743

This theorem is referenced by:  sbceq1d  3747  sbc8g  3750  spsbc  3755  sbccow  3765  sbcco  3768  sbcco2  3769  sbcie2g  3783  elrabsf  3788  eqsbc1  3789  csbeq1  3854  cbvralcsf  3893  sbcnestgfw  4375  sbcco3gw  4379  sbcnestgf  4380  sbcco3g  4384  csbie2df  4397  reusngf  4633  reuprg0  4661  sbcop  5445  reuop  6259  ralrnmptw  7048  ralrnmpt  7050  tfindes  7815  findcard2  9101  ac6sfi  9196  indexfi  9272  nn1suc  12179  uzind4s2  12834  wrdind  14657  wrd2ind  14658  prmind2  16624  mndind  18765  elmptrab  23783  isfildlem  23813  ifeqeqx  32628  wrdt2ind  33045  bnj609  35092  bnj601  35095  weiunlem  36676  sdclem2  37982  fdc1  37986  sbccom2  38365  sbccom2f  38366  sbccom2fi  38367  elimhyps  39326  dedths  39327  elimhyps2  39329  dedths2  39330  lshpkrlem3  39477  rexrabdioph  43140  rexfrabdioph  43141  2rexfrabdioph  43142  3rexfrabdioph  43143  4rexfrabdioph  43144  6rexfrabdioph  43145  7rexfrabdioph  43146  2nn0ind  43291  zindbi  43292  axfrege52c  44232  frege58c  44266  frege92  44300  2sbc6g  44760  2sbc5g  44761  pm14.122b  44768  pm14.24  44777  iotavalsb  44778  sbiota1  44779  fvsb  44796  or2expropbilem1  47381  ich2exprop  47820  reupr  47871