ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfsbcq2 GIF version

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2203 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2127 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 2913 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 131 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 221 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1332  wcel 1481  [wsb 1736  {cab 2126  [wsbc 2912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-clab 2127  df-cleq 2133  df-clel 2136  df-sbc 2913
This theorem is referenced by:  sbsbc  2916  sbc8g  2919  sbceq1a  2921  sbc5  2935  sbcng  2952  sbcimg  2953  sbcan  2954  sbcang  2955  sbcor  2956  sbcorg  2957  sbcbig  2958  sbcal  2963  sbcalg  2964  sbcex2  2965  sbcexg  2966  sbcel1v  2974  sbctt  2978  sbcralt  2988  sbcrext  2989  sbcralg  2990  sbcreug  2992  rspsbc  2994  rspesbca  2996  sbcel12g  3021  sbceqg  3022  sbcbrg  3989  csbopabg  4013  opelopabsb  4189  findes  4524  iota4  5113  csbiotag  5123  csbriotag  5749  nn0ind-raph  9191  uzind4s  9411  bezoutlemmain  11720  bezoutlemex  11723
  Copyright terms: Public domain W3C validator