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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2880 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2780 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 3724 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 227 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 316 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  [wsb 2069  wcel 2112  {cab 2779  [wsbc 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clab 2780  df-cleq 2794  df-clel 2873  df-sbc 3724
This theorem is referenced by:  sbsbc  3727  sbc8g  3731  sbc2or  3732  sbceq1a  3734  sbc5  3751  sbcng  3769  sbcimg  3770  sbcan  3771  sbcor  3772  sbcbig  3773  sbcal  3783  sbcex2  3784  sbcel1v  3789  sbctt  3793  sbcralt  3804  sbcreu  3808  rspsbc  3811  rspesbca  3813  csb0  4317  sbcel12  4319  sbceqg  4320  csbif  4483  rexreusng  4580  sbcbr123  5087  opelopabsb  5385  csbopab  5410  csbopabgALT  5411  iota4  6309  csbiota  6321  csbriota  7112  onminex  7506  findes  7597  nn0ind-raph  12074  uzind4s  12300  nn0min  30566  sbcrexgOLD  39719
  Copyright terms: Public domain W3C validator