Theorem dfsbcq 3749

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

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  {cab 2743  [wsbc 3747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840  df-sbc 3748

This theorem is referenced by:  sbceq1d  3752  sbc8g  3755  spsbc  3760  sbccow  3770  sbcco  3773  sbcco2  3774  sbcie2g  3787  elrabsf  3792  eqsbc1  3793  csbeq1  3858  cbvralcsf  3897  sbcnestgfw  4378  sbcco3gw  4382  sbcnestgf  4383  sbcco3g  4387  csbie2df  4400  reusngf  4636  reuprg0  4664  sbcop  5462  reuop  6284  ralrnmptw  7079  ralrnmpt  7081  tfindes  7847  findcard2  9137  ac6sfi  9232  indexfi  9305  nn1suc  12246  uzind4s2  12924  wrdind  14749  wrd2ind  14750  prmind2  16733  mndind  18877  elmptrab  23945  isfildlem  23975  ifeqeqx  32798  wrdt2ind  33186  bnj609  35222  bnj601  35225  weiunlem  36836  sdclem2  38253  fdc1  38257  sbccom2  38636  sbccom2f  38637  sbccom2fi  38638  elimhyps  39597  dedths  39598  elimhyps2  39600  dedths2  39601  lshpkrlem3  39748  rexrabdioph  43383  rexfrabdioph  43384  2rexfrabdioph  43385  3rexfrabdioph  43386  4rexfrabdioph  43387  6rexfrabdioph  43388  7rexfrabdioph  43389  2nn0ind  43534  zindbi  43535  axfrege52c  44475  frege58c  44509  frege92  44543  2sbc6g  44989  2sbc5g  44990  pm14.122b  44997  pm14.24  45006  iotavalsb  45007  sbiota1  45008  fvsb  45025  or2expropbilem1  47624  ich2exprop  48075  reupr  48126