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

Theorem sbceqbid 3705
 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 2822 . . 3 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
41, 3eleq12d 2846 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝐵 ∈ {𝑥𝜒}))
5 df-sbc 3699 . 2 ([𝐴 / 𝑥]𝜓𝐴 ∈ {𝑥𝜓})
6 df-sbc 3699 . 2 ([𝐵 / 𝑥]𝜒𝐵 ∈ {𝑥𝜒})
74, 5, 63bitr4g 317 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {cab 2735  [wsbc 3698 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-sbc 3699 This theorem is referenced by:  sbcbidv  3753  fpwwe2cbv  10103  fpwwe2lem2  10105  fpwwe2lem3  10106  fi1uzind  13920  isprs  17619  isdrs  17623  istos  17724  isdlat  17882  issrg  19338  islmod  19719  frpoins3xpg  33344  frpoins3xp3g  33345  fdc  35497  hdmap1ffval  39405  hdmap1fval  39406  hdmapffval  39436  hdmapfval  39437  hgmapffval  39495  hgmapfval  39496  sbccomieg  40142  rexrabdioph  40143
 Copyright terms: Public domain W3C validator