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

Theorem sbceqbid 3794
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 2807 . . 3 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
41, 3eleq12d 2834 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝐵 ∈ {𝑥𝜒}))
5 df-sbc 3788 . 2 ([𝐴 / 𝑥]𝜓𝐴 ∈ {𝑥𝜓})
6 df-sbc 3788 . 2 ([𝐵 / 𝑥]𝜒𝐵 ∈ {𝑥𝜒})
74, 5, 63bitr4g 314 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1539  wcel 2107  {cab 2713  [wsbc 3787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-sbc 3788
This theorem is referenced by:  sbcbidv  3844  frpoins3xpg  8166  frpoins3xp3g  8167  fpwwe2cbv  10671  fpwwe2lem2  10673  fpwwe2lem3  10674  fi1uzind  14547  isprs  18343  isdrs  18348  istos  18464  isdlat  18568  issrg  20186  islmod  20863  fdc  37753  hdmap1ffval  41798  hdmap1fval  41799  hdmapffval  41829  hdmapfval  41830  hgmapffval  41888  hgmapfval  41889  sbccomieg  42809  rexrabdioph  42810
  Copyright terms: Public domain W3C validator