Theorem dfsbcq 2957

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 2956 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 2958 instead of df-sbc 2956. (dfsbcq2 2958 is needed because unlike Quine we do not overload the df-sb 1756 syntax.) As a consequence of these theorems, we can derive sbc8g 2962, which is a weaker version of df-sbc 2956 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 2962, so we will allow direct use of df-sbc 2956. 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 2233	. 2 |- ( A = B -> ( A e. { x | ph } <-> B e. { x | ph } ) )
2		df-sbc 2956	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
3		df-sbc 2956	. 2 |- ( [. B / x ]. ph <-> B e. { x | ph } )
4	1, 2, 3	3bitr4g 222	1 |- ( A = B -> ( [. A / x ]. ph <-> [. B / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   e. wcel 2141   {cab 2156   [.wsbc 2955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-sbc 2956

This theorem is referenced by:  sbceq1d  2960  sbc8g  2962  spsbc  2966  sbcco  2976  sbcco2  2977  sbcie2g  2988  elrabsf  2993  eqsbc1  2994  csbeq1  3052  sbcnestgf  3100  sbcco3g  3106  cbvralcsf  3111  cbvrexcsf  3112  findes  4587  ralrnmpt  5638  rexrnmpt  5639  findcard2  6867  findcard2s  6868  ac6sfi  6876  nn1suc  8897  uzind4s2  9550  indstr  9552  bezoutlemmain  11953  prmind2  12074