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

Theorem dfsbcq 3172
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 3171 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 3173 instead of df-sbc 3171. (dfsbcq2 3173 is needed because unlike Quine we do not overload the df-sb 1661 syntax.) As a consequence of these theorems, we can derive sbc8g 3177, which is a weaker version of df-sbc 3171 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 3177, so we will allow direct use of df-sbc 3171 after theorem sbc2or 3178 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 2503 . 2  |-  ( A  =  B  ->  ( A  e.  { x  |  ph }  <->  B  e.  { x  |  ph }
) )
2 df-sbc 3171 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
3 df-sbc 3171 . 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 4    <-> wb 178    = wceq 1654    e. wcel 1728   {cab 2429   [.wsbc 3170
This theorem is referenced by:  sbceq1d  3175  sbc8g  3177  spsbc  3182  sbcco  3192  sbcco2  3193  sbcie2g  3203  elrabsf  3208  eqsbc3  3209  csbeq1  3273  cbvralcsf  3300  sbcnestgf  3669  sbcco3g  3674  tfindes  4877  findes  4910  ralrnmpt  5914  findcard2  7384  ac6sfi  7387  indexfi  7450  ac6num  8397  fpwwe2cbv  8543  fpwwe2lem2  8545  fpwwe2lem3  8546  nn1suc  10059  uzindOLD  10402  uzind4s  10574  uzind4s2  10575  fzrevral  11169  fzshftral  11172  wrdind  11829  cjth  11946  prmind2  13128  isprs  14425  isdrs  14429  joinlem  14485  meetlem  14492  istos  14502  isdlat  14657  gsumvalx  14812  islmod  15992  elmptrab  17897  isfildlem  17927  quotval  20247  ifeqeqx  24037  sdclem2  26488  fdc  26491  fdc1  26492  sbccomieg  26961  rexrabdioph  26966  rexfrabdioph  26967  2rexfrabdioph  26968  3rexfrabdioph  26969  4rexfrabdioph  26970  6rexfrabdioph  26971  7rexfrabdioph  26972  2nn0ind  27120  zindbi  27121  2sbc6g  27704  2sbc5g  27705  pm14.122b  27712  pm14.24  27721  iotavalsb  27722  sbiota1  27723  iotasbcq  27726  fvsb  27743  bnj609  29462  bnj601  29465  bnj944  29483  lshpkrlem3  30084  hdmap1ffval  32768  hdmap1fval  32769  hdmapffval  32801  hdmapfval  32802  hgmapffval  32860  hgmapfval  32861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-11 1764  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2436  df-clel 2439  df-sbc 3171
  Copyright terms: Public domain W3C validator