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

Theorem dfsbcq2 3405
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 1868 and substitution for class variables df-sbc 3403. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3404. (Contributed by NM, 31-Dec-2016.)
Assertion
Ref Expression
dfsbcq2 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2676 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2597 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 3403 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 213 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 301 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  [wsb 1867  wcel 1977  {cab 2596  [wsbc 3402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403
This theorem is referenced by:  sbsbc  3406  sbc8g  3410  sbc2or  3411  sbceq1a  3413  sbc5  3427  sbcng  3443  sbcimg  3444  sbcan  3445  sbcor  3446  sbcbig  3447  sbcal  3452  sbcex2  3453  sbcel1v  3462  sbctt  3467  sbcralt  3477  sbcreu  3482  rspsbc  3484  rspesbca  3486  sbcel12  3935  sbceqg  3936  csbif  4088  sbcbr123  4636  opelopabsb  4910  csbopab  4932  csbopabgALT  4933  iota4  5786  csbiota  5797  csbriota  6523  onminex  6899  findes  6988  nn0ind-raph  11353  uzind4s  11624  nn0min  28954  sbcrexgOLD  36367  sbcangOLD  37760  sbcorgOLD  37761  sbcalgOLD  37773  sbcexgOLD  37774  sbcel12gOLD  37775  sbcel1gvOLD  38116
  Copyright terms: Public domain W3C validator