Theorem dfsbcq 2766

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

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1243   e. wcel 1393   {cab 2026   [.wsbc 2764

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-sbc 2765

This theorem is referenced by:  sbceq1d  2769  sbc8g  2771  spsbc  2775  sbcco  2785  sbcco2  2786  sbcie2g  2796  elrabsf  2801  eqsbc3  2802  csbeq1  2855  sbcnestgf  2897  sbcco3g  2903  cbvralcsf  2908  cbvrexcsf  2909  findes  4326  ralrnmpt  5309  rexrnmpt  5310  findcard2  6346  findcard2s  6347  ac6sfi  6352  nn1suc  7933  uzind4s2  8534  indstr  8536