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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2819 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2708 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 3777 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 223 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 312 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  [wsb 2065  wcel 2104  {cab 2707  [wsbc 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-clab 2708  df-cleq 2722  df-clel 2808  df-sbc 3777
This theorem is referenced by:  sbsbc  3780  sbc8g  3784  sbc2or  3785  sbceq1a  3787  sbc5ALT  3805  sbcng  3826  sbcimg  3827  sbcan  3828  sbcor  3829  sbcbig  3830  sbcim1  3832  sbcal  3840  sbcex2  3841  sbcel1v  3847  sbctt  3852  sbcralt  3865  sbcreu  3869  rspsbc  3872  rspesbca  3874  sbcel12  4407  sbceqg  4408  csbif  4584  rexreusng  4682  sbcbr123  5201  opelopabsb  5529  csbopab  5554  csbopabgALT  5555  iota4  6523  csbiota  6535  csbriota  7383  onminex  7792  findes  7895  nn0ind-raph  12666  uzind4s  12896  nn0min  32293  sbcrexgOLD  41825
  Copyright terms: Public domain W3C validator