Theorem dfsbcq 2953

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 2952 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 2954 instead of df-sbc 2952. (dfsbcq2 2954 is needed because unlike Quine we do not overload the df-sb 1751 syntax.) As a consequence of these theorems, we can derive sbc8g 2958, which is a weaker version of df-sbc 2952 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 2958, so we will allow direct use of df-sbc 2952. 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 2229	. 2 |- ( A = B -> ( A e. { x | ph } <-> B e. { x | ph } ) )
2		df-sbc 2952	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
3		df-sbc 2952	. 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 1343   e. wcel 2136   {cab 2151   [.wsbc 2951

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-sbc 2952

This theorem is referenced by:  sbceq1d  2956  sbc8g  2958  spsbc  2962  sbcco  2972  sbcco2  2973  sbcie2g  2984  elrabsf  2989  eqsbc1  2990  csbeq1  3048  sbcnestgf  3096  sbcco3g  3102  cbvralcsf  3107  cbvrexcsf  3108  findes  4580  ralrnmpt  5627  rexrnmpt  5628  findcard2  6855  findcard2s  6856  ac6sfi  6864  nn1suc  8876  uzind4s2  9529  indstr  9531  bezoutlemmain  11931  prmind2  12052