Theorem dfsbcq 3777

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

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

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

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 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806  df-sbc 3776

This theorem is referenced by:  sbceq1d  3780  sbc8g  3783  spsbc  3788  sbccow  3798  sbcco  3801  sbcco2  3802  sbcie2g  3817  elrabsf  3823  eqsbc1  3824  csbeq1  3893  cbvralcsf  3935  sbcnestgfw  4415  sbcco3gw  4419  sbcnestgf  4420  sbcco3g  4424  csbie2df  4437  reusngf  4673  reuprg0  4703  sbcop  5486  reuop  6292  ralrnmptw  7099  ralrnmpt  7101  tfindes  7862  findcard2  9183  findcard2OLD  9303  ac6sfi  9306  indexfi  9379  nn1suc  12259  uzind4s2  12918  wrdind  14699  wrd2ind  14700  prmind2  16650  mndind  18774  elmptrab  23725  isfildlem  23755  ifeqeqx  32327  wrdt2ind  32669  bnj609  34543  bnj601  34546  sdclem2  37210  fdc1  37214  sbccom2  37593  sbccom2f  37594  sbccom2fi  37595  elimhyps  38428  dedths  38429  elimhyps2  38431  dedths2  38432  lshpkrlem3  38579  rexrabdioph  42205  rexfrabdioph  42206  2rexfrabdioph  42207  3rexfrabdioph  42208  4rexfrabdioph  42209  6rexfrabdioph  42210  7rexfrabdioph  42211  2nn0ind  42357  zindbi  42358  axfrege52c  43308  frege58c  43342  frege92  43376  2sbc6g  43843  2sbc5g  43844  pm14.122b  43851  pm14.24  43860  iotavalsb  43861  sbiota1  43862  fvsb  43880  or2expropbilem1  46405  ich2exprop  46802  reupr  46853

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »