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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2150 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2075 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 2839 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 130 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 220 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1289  wcel 1438  [wsb 1692  {cab 2074  [wsbc 2838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-clab 2075  df-cleq 2081  df-clel 2084  df-sbc 2839
This theorem is referenced by:  sbsbc  2842  sbc8g  2845  sbceq1a  2847  sbc5  2861  sbcng  2877  sbcimg  2878  sbcan  2879  sbcang  2880  sbcor  2881  sbcorg  2882  sbcbig  2883  sbcal  2888  sbcalg  2889  sbcex2  2890  sbcexg  2891  sbcel1v  2899  sbctt  2903  sbcralt  2913  sbcrext  2914  sbcralg  2915  sbcreug  2917  rspsbc  2919  rspesbca  2921  sbcel12g  2944  sbceqg  2945  sbcbrg  3886  csbopabg  3908  opelopabsb  4078  findes  4408  iota4  4985  csbiotag  4995  csbriotag  5602  nn0ind-raph  8833  uzind4s  9047  bezoutlemmain  11080  bezoutlemex  11083
  Copyright terms: Public domain W3C validator