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

Theorem sbceqbid 3784
Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)
Hypotheses
Ref Expression
sbceqbid.1 (𝜑𝐴 = 𝐵)
sbceqbid.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
sbceqbid (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem sbceqbid
StepHypRef Expression
1 sbceqbid.1 . . 3 (𝜑𝐴 = 𝐵)
2 sbceqbid.2 . . . 4 (𝜑 → (𝜓𝜒))
32abbidv 2801 . . 3 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
41, 3eleq12d 2827 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝐵 ∈ {𝑥𝜒}))
5 df-sbc 3778 . 2 ([𝐴 / 𝑥]𝜓𝐴 ∈ {𝑥𝜓})
6 df-sbc 3778 . 2 ([𝐵 / 𝑥]𝜒𝐵 ∈ {𝑥𝜒})
74, 5, 63bitr4g 313 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  {cab 2709  [wsbc 3777
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3778
This theorem is referenced by:  sbcbidv  3836  frpoins3xpg  8128  frpoins3xp3g  8129  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwe2lem3  10630  fi1uzind  14460  isprs  18252  isdrs  18256  istos  18373  isdlat  18477  issrg  20013  islmod  20479  fdc  36699  hdmap1ffval  40752  hdmap1fval  40753  hdmapffval  40783  hdmapfval  40784  hgmapffval  40842  hgmapfval  40843  sbccomieg  41613  rexrabdioph  41614
  Copyright terms: Public domain W3C validator