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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2116 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2043 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 2788 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 127 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 215 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102   = wceq 1259  wcel 1409  [wsb 1661  {cab 2042  [wsbc 2787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-clab 2043  df-cleq 2049  df-clel 2052  df-sbc 2788
This theorem is referenced by:  sbsbc  2791  sbc8g  2794  sbceq1a  2796  sbc5  2810  sbcng  2826  sbcimg  2827  sbcan  2828  sbcang  2829  sbcor  2830  sbcorg  2831  sbcbig  2832  sbcal  2837  sbcalg  2838  sbcex2  2839  sbcexg  2840  sbcel1v  2848  sbctt  2852  sbcralt  2862  sbcrext  2863  sbcralg  2864  sbcreug  2866  rspsbc  2868  rspesbca  2870  sbcel12g  2893  sbceqg  2894  sbcbrg  3841  csbopabg  3863  opelopabsb  4025  findes  4354  iota4  4913  csbiotag  4923  csbriotag  5508  nn0ind-raph  8414  uzind4s  8629
  Copyright terms: Public domain W3C validator