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

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

Proof of Theorem dfsbcq2
StepHypRef Expression
1 eleq1 2718 . 2 (𝑦 = 𝐴 → (𝑦 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
2 df-clab 2638 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-sbc 3469 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
43bicomi 214 . 2 (𝐴 ∈ {𝑥𝜑} ↔ [𝐴 / 𝑥]𝜑)
51, 2, 43bitr3g 302 1 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  [wsb 1937  wcel 2030  {cab 2637  [wsbc 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-clab 2638  df-cleq 2644  df-clel 2647  df-sbc 3469
This theorem is referenced by:  sbsbc  3472  sbc8g  3476  sbc2or  3477  sbceq1a  3479  sbc5  3493  sbcng  3509  sbcimg  3510  sbcan  3511  sbcor  3512  sbcbig  3513  sbcal  3518  sbcex2  3519  sbcel1v  3528  sbctt  3533  sbcralt  3543  sbcreu  3548  rspsbc  3551  rspesbca  3553  sbcel12  4016  sbceqg  4017  csbif  4171  sbcbr123  4739  opelopabsb  5014  csbopab  5037  csbopabgALT  5038  iota4  5907  csbiota  5919  csbriota  6663  onminex  7049  findes  7138  nn0ind-raph  11515  uzind4s  11786  nn0min  29695  sbcrexgOLD  37666  sbcangOLD  39056  sbcorgOLD  39057  sbcalgOLD  39069  sbcexgOLD  39070  sbcel12gOLD  39071  sbcel1gvOLD  39408
  Copyright terms: Public domain W3C validator