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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2873 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2793 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 3634 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 215 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 304 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  [wsb 2060  wcel 2156  {cab 2792  [wsbc 3633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-clab 2793  df-cleq 2799  df-clel 2802  df-sbc 3634
This theorem is referenced by:  sbsbc  3637  sbc8g  3641  sbc2or  3642  sbceq1a  3644  sbc5  3658  sbcng  3674  sbcimg  3675  sbcan  3676  sbcor  3677  sbcbig  3678  sbcal  3683  sbcex2  3684  sbcel1v  3692  sbctt  3696  sbcralt  3706  sbcreu  3710  rspsbc  3713  rspesbca  3715  sbcel12  4180  sbceqg  4181  csbif  4334  sbcbr123  4898  opelopabsb  5180  csbopab  5203  csbopabgALT  5204  iota4  6078  csbiota  6090  csbriota  6843  onminex  7233  findes  7322  nn0ind-raph  11739  uzind4s  11962  nn0min  29893  sbcrexgOLD  37848  sbcangOLD  39234  sbcorgOLD  39235  sbcalgOLD  39247  sbcexgOLD  39248  sbcel12gOLD  39249  sbcel1gvOLD  39585
  Copyright terms: Public domain W3C validator