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

Theorem cbviotavw 6524
Description: Change bound variables in a description binder. Version of cbviotav 6526 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.)
Hypothesis
Ref Expression
cbviotavw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbviotavw (℩𝑥𝜑) = (℩𝑦𝜓)
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbviotavw
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cbviotavw.1 . . . . . 6 (𝑥 = 𝑦 → (𝜑𝜓))
21cbvabv 2810 . . . . 5 {𝑥𝜑} = {𝑦𝜓}
32eqeq1i 2740 . . . 4 ({𝑥𝜑} = {𝑧} ↔ {𝑦𝜓} = {𝑧})
43abbii 2807 . . 3 {𝑧 ∣ {𝑥𝜑} = {𝑧}} = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
54unieqi 4924 . 2 {𝑧 ∣ {𝑥𝜑} = {𝑧}} = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
6 df-iota 6516 . 2 (℩𝑥𝜑) = {𝑧 ∣ {𝑥𝜑} = {𝑧}}
7 df-iota 6516 . 2 (℩𝑦𝜓) = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
85, 6, 73eqtr4i 2773 1 (℩𝑥𝜑) = (℩𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1537  {cab 2712  {csn 4631   cuni 4912  cio 6514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-iota 6516
This theorem is referenced by:  cbvriotavw  7398  oeeui  8639  nosupcbv  27762  noinfcbv  27777  cbvriotavw2  36219  ellimciota  45570  fourierdlem96  46158  fourierdlem97  46159  fourierdlem98  46160  fourierdlem99  46161  fourierdlem105  46167  fourierdlem106  46168  fourierdlem108  46170  fourierdlem110  46172  fourierdlem112  46174  fourierdlem113  46175  fourierdlem115  46177  funressndmafv2rn  47173
  Copyright terms: Public domain W3C validator