MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfsbcq Unicode version

Theorem dfsbcq 2954
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 2953 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 2955 instead of df-sbc 2953. (dfsbcq2 2955 is needed because unlike Quine we do not overload the df-sb 1884 syntax.) As a consequence of these theorems, we can derive sbc8g 2959, which is a weaker version of df-sbc 2953 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 2959, so we will allow direct use of df-sbc 2953 after theorem sbc2or 2960 below. 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 2316 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 2953 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 2953 . 2  |-  ( [. B  /  x ]. ph  <->  B  e.  { x  |  ph }
)
41, 2, 33bitr4g 281 1  |-  ( A  =  B  ->  ( [. A  /  x ]. ph  <->  [. B  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   {cab 2242   [.wsbc 2952
This theorem is referenced by:  sbceq1d  2957  sbc8g  2959  a4sbc  2964  sbcco  2974  sbcco2  2975  sbcie2g  2985  elrabsf  2990  eqsbc3  2991  csbeq1  3045  sbcnestgf  3089  sbcco3g  3097  cbvralcsf  3104  tfindes  4611  findes  4644  ralrnmpt  5589  findcard2  7052  ac6sfi  7055  indexfi  7117  ac6num  8060  fpwwe2cbv  8206  fpwwe2lem2  8208  fpwwe2lem3  8209  nn1suc  9721  uzindOLD  10059  uzind4s  10231  uzind4s2  10232  fzrevral  10818  fzshftral  10821  wrdind  11428  cjth  11539  prmind2  12717  isprs  14012  isdrs  14016  joinlem  14072  meetlem  14079  istos  14089  isdlat  14244  gsumvalx  14399  islmod  15579  elmptrab  17470  isfildlem  17500  quotval  19620  ifeqeqx  22980  sbcbidv2  24321  bisig0  25415  isibg2  25463  sdclem2  25805  fdc  25808  fdc1  25809  sbccomieg  26223  rexrabdioph  26228  rexfrabdioph  26229  2rexfrabdioph  26230  3rexfrabdioph  26231  4rexfrabdioph  26232  6rexfrabdioph  26233  7rexfrabdioph  26234  2nn0ind  26383  zindbi  26384  2sbc6g  26969  2sbc5g  26970  pm14.122b  26977  pm14.24  26986  iotavalsb  26987  sbiota1  26988  iotasbcq  26991  fvsb  27009  bnj609  27982  bnj601  27985  bnj944  28003  lshpkrlem3  28453  hdmap1ffval  31137  hdmap1fval  31138  hdmapffval  31170  hdmapfval  31171  hgmapffval  31229  hgmapfval  31230
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-cleq 2249  df-clel 2252  df-sbc 2953
  Copyright terms: Public domain W3C validator