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

Theorem dfsbcq 2884
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 2883 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 2885 instead of df-sbc 2883. (dfsbcq2 2885 is needed because unlike Quine we do not overload the df-sb 1721 syntax.) As a consequence of these theorems, we can derive sbc8g 2889, which is a weaker version of df-sbc 2883 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 2889, so we will allow direct use of df-sbc 2883. 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 2180 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 2883 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 2883 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 222 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316    e. wcel 1465   {cab 2103   [.wsbc 2882
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113  df-sbc 2883
This theorem is referenced by:  sbceq1d  2887  sbc8g  2889  spsbc  2893  sbcco  2903  sbcco2  2904  sbcie2g  2914  elrabsf  2919  eqsbc3  2920  csbeq1  2978  sbcnestgf  3021  sbcco3g  3027  cbvralcsf  3032  cbvrexcsf  3033  findes  4487  ralrnmpt  5530  rexrnmpt  5531  findcard2  6751  findcard2s  6752  ac6sfi  6760  nn1suc  8703  uzind4s2  9342  indstr  9344  bezoutlemmain  11598  prmind2  11713
  Copyright terms: Public domain W3C validator