Theorem dfsbcq 3033

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 3032 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 3034 instead of df-sbc 3032. (dfsbcq2 3034 is needed because unlike Quine we do not overload the df-sb 1811 syntax.) As a consequence of these theorems, we can derive sbc8g 3039, which is a weaker version of df-sbc 3032 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 3039, so we will allow direct use of df-sbc 3032. 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 3032	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
3		df-sbc 3032	. 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 1397   e. wcel 2202   {cab 2217   [.wsbc 3031

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  sbceq1d  3036  sbc8g  3039  spsbc  3043  sbcco  3053  sbcco2  3054  sbcie2g  3065  elrabsf  3070  eqsbc1  3071  csbeq1  3130  sbcnestgf  3179  sbcco3g  3185  cbvralcsf  3190  cbvrexcsf  3191  findes  4701  ralrnmpt  5789  rexrnmpt  5790  uchoice  6299  findcard2  7077  findcard2s  7078  ac6sfi  7086  nn1suc  9161  uzind4s2  9824  indstr  9826  wrdind  11302  wrd2ind  11303  bezoutlemmain  12568  prmind2  12691