ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfsbcq Unicode version

Theorem dfsbcq 2964
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 2963 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 2965 instead of df-sbc 2963. (dfsbcq2 2965 is needed because unlike Quine we do not overload the df-sb 1763 syntax.) As a consequence of these theorems, we can derive sbc8g 2970, which is a weaker version of df-sbc 2963 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 2970, so we will allow direct use of df-sbc 2963. 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
StepHypRef Expression
1 eleq1 2240 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 2963 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 2963 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 223 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    = wceq 1353    e. wcel 2148   {cab 2163   [.wsbc 2962
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-sbc 2963
This theorem is referenced by:  sbceq1d  2967  sbc8g  2970  spsbc  2974  sbcco  2984  sbcco2  2985  sbcie2g  2996  elrabsf  3001  eqsbc1  3002  csbeq1  3060  sbcnestgf  3108  sbcco3g  3114  cbvralcsf  3119  cbvrexcsf  3120  findes  4598  ralrnmpt  5653  rexrnmpt  5654  findcard2  6882  findcard2s  6883  ac6sfi  6891  nn1suc  8914  uzind4s2  9567  indstr  9569  bezoutlemmain  11969  prmind2  12090
  Copyright terms: Public domain W3C validator