MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfsbcq2 Structured version   Visualization version   GIF version

Theorem dfsbcq2 3404
Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb 1867 and substitution for class variables df-sbc 3402. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3403. (Contributed by NM, 31-Dec-2016.)
Assertion
Ref Expression
dfsbcq2 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2675 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2596 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 3402 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 212 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 300 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  [wsb 1866  wcel 1976  {cab 2595  [wsbc 3401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-clab 2596  df-cleq 2602  df-clel 2605  df-sbc 3402
This theorem is referenced by:  sbsbc  3405  sbc8g  3409  sbc2or  3410  sbceq1a  3412  sbc5  3426  sbcng  3442  sbcimg  3443  sbcan  3444  sbcor  3445  sbcbig  3446  sbcal  3451  sbcex2  3452  sbcel1v  3461  sbctt  3466  sbcralt  3476  sbcreu  3481  rspsbc  3483  rspesbca  3485  sbcel12  3934  sbceqg  3935  csbif  4087  sbcbr123  4630  opelopabsb  4900  csbopab  4922  csbopabgALT  4923  iota4  5772  csbiota  5783  csbriota  6501  onminex  6876  findes  6965  nn0ind-raph  11309  uzind4s  11580  nn0min  28760  sbcrexgOLD  36170  sbcangOLD  37563  sbcorgOLD  37564  sbcalgOLD  37576  sbcexgOLD  37577  sbcel12gOLD  37578  sbcel1gvOLD  37919
  Copyright terms: Public domain W3C validator