Theorem dfsbcq 3034

Description: 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 3033 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 3035 instead of df-sbc 3033. (dfsbcq2 3035 is needed because unlike Quine we do not overload the df-sb 1811 syntax.) As a consequence of these theorems, we can derive sbc8g 3040, which is a weaker version of df-sbc 3033 that leaves substitution undefined when A is a proper class.

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3040, so we will allow direct use of df-sbc 3033. Proper substiution 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	|- ( A = B -> ( [. A / x ]. ph <-> [. B / x ]. ph ) )

Proof of Theorem dfsbcq

Step	Hyp	Ref	Expression
1		eleq1 2294	. 2 |- ( A = B -> ( A e. { x | ph } <-> B e. { x | ph } ) )
2		df-sbc 3033	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
3		df-sbc 3033	. 2 |- ( [. B / x ]. ph <-> B e. { x | ph } )
4	1, 2, 3	3bitr4g 223	1 |- ( A = B -> ( [. A / x ]. ph <-> [. B / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2202   {cab 2217   [.wsbc 3032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-sbc 3033

This theorem is referenced by:  sbceq1d  3037  sbc8g  3040  spsbc  3044  sbcco  3054  sbcco2  3055  sbcie2g  3066  elrabsf  3071  eqsbc1  3072  csbeq1  3131  sbcnestgf  3180  sbcco3g  3186  cbvralcsf  3191  cbvrexcsf  3192  findes  4707  ralrnmpt  5797  rexrnmpt  5798  uchoice  6309  findcard2  7121  findcard2s  7122  ac6sfi  7130  nn1suc  9204  uzind4s2  9869  indstr  9871  wrdind  11352  wrd2ind  11353  bezoutlemmain  12632  prmind2  12755