Theorem dfsbcq 2864

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 2863 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 2865 instead of df-sbc 2863. (dfsbcq2 2865 is needed because unlike Quine we do not overload the df-sb 1704 syntax.) As a consequence of these theorems, we can derive sbc8g 2869, which is a weaker version of df-sbc 2863 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 2869, so we will allow direct use of df-sbc 2863. 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 2162	. 2 |- ( A = B -> ( A e. { x | ph } <-> B e. { x | ph } ) )
2		df-sbc 2863	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
3		df-sbc 2863	. 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 1299   e. wcel 1448   {cab 2086   [.wsbc 2862

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096  df-sbc 2863

This theorem is referenced by:  sbceq1d  2867  sbc8g  2869  spsbc  2873  sbcco  2883  sbcco2  2884  sbcie2g  2894  elrabsf  2899  eqsbc3  2900  csbeq1  2958  sbcnestgf  3001  sbcco3g  3007  cbvralcsf  3012  cbvrexcsf  3013  findes  4455  ralrnmpt  5494  rexrnmpt  5495  findcard2  6712  findcard2s  6713  ac6sfi  6721  nn1suc  8597  uzind4s2  9236  indstr  9238  bezoutlemmain  11479  prmind2  11594