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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2688 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2608 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 3434 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 214 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 302 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1482  [wsb 1879  wcel 1989  {cab 2607  [wsbc 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-clab 2608  df-cleq 2614  df-clel 2617  df-sbc 3434
This theorem is referenced by:  sbsbc  3437  sbc8g  3441  sbc2or  3442  sbceq1a  3444  sbc5  3458  sbcng  3474  sbcimg  3475  sbcan  3476  sbcor  3477  sbcbig  3478  sbcal  3483  sbcex2  3484  sbcel1v  3493  sbctt  3498  sbcralt  3508  sbcreu  3513  rspsbc  3516  rspesbca  3518  sbcel12  3981  sbceqg  3982  csbif  4136  sbcbr123  4704  opelopabsb  4983  csbopab  5006  csbopabgALT  5007  iota4  5867  csbiota  5879  csbriota  6620  onminex  7004  findes  7093  nn0ind-raph  11474  uzind4s  11745  nn0min  29552  sbcrexgOLD  37175  sbcangOLD  38565  sbcorgOLD  38566  sbcalgOLD  38578  sbcexgOLD  38579  sbcel12gOLD  38580  sbcel1gvOLD  38920
  Copyright terms: Public domain W3C validator