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

Theorem cbvab 2733
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
Hypotheses
Ref Expression
cbvab.1 𝑦𝜑
cbvab.2 𝑥𝜓
cbvab.3 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvab {𝑥𝜑} = {𝑦𝜓}

Proof of Theorem cbvab
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cbvab.1 . . . . 5 𝑦𝜑
21sbco2 2403 . . . 4 ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
3 cbvab.2 . . . . . 6 𝑥𝜓
4 cbvab.3 . . . . . 6 (𝑥 = 𝑦 → (𝜑𝜓))
53, 4sbie 2396 . . . . 5 ([𝑦 / 𝑥]𝜑𝜓)
65sbbii 1874 . . . 4 ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
72, 6bitr3i 265 . . 3 ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
8 df-clab 2597 . . 3 (𝑧 ∈ {𝑥𝜑} ↔ [𝑧 / 𝑥]𝜑)
9 df-clab 2597 . . 3 (𝑧 ∈ {𝑦𝜓} ↔ [𝑧 / 𝑦]𝜓)
107, 8, 93bitr4i 291 . 2 (𝑧 ∈ {𝑥𝜑} ↔ 𝑧 ∈ {𝑦𝜓})
1110eqriv 2607 1 {𝑥𝜑} = {𝑦𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  Ⅎwnf 1699  [wsb 1867   ∈ wcel 1977  {cab 2596 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603 This theorem is referenced by:  cbvabv  2734  cbvrab  3171  cbvsbc  3431  cbvrabcsf  3534  rabsnifsb  4201  rabasiun  4459  dfdmf  5239  dfrnf  5285  funfv2f  6177  abrexex2g  7036  abrexex2  7040  bnj873  30248  ptrest  32578  poimirlem26  32605  poimirlem27  32606
 Copyright terms: Public domain W3C validator