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

Theorem cbviotavw 6521
Description: Change bound variables in a description binder. Version of cbviotav 6523 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 2811 . . . . 5 {𝑥𝜑} = {𝑦𝜓}
32eqeq1i 2741 . . . 4 ({𝑥𝜑} = {𝑧} ↔ {𝑦𝜓} = {𝑧})
43abbii 2808 . . 3 {𝑧 ∣ {𝑥𝜑} = {𝑧}} = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
54unieqi 4918 . 2 {𝑧 ∣ {𝑥𝜑} = {𝑧}} = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
6 df-iota 6513 . 2 (℩𝑥𝜑) = {𝑧 ∣ {𝑥𝜑} = {𝑧}}
7 df-iota 6513 . 2 (℩𝑦𝜓) = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
85, 6, 73eqtr4i 2774 1 (℩𝑥𝜑) = (℩𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1539  {cab 2713  {csn 4625   cuni 4906  cio 6511
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-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-uni 4907  df-iota 6513
This theorem is referenced by:  cbvriotavw  7399  oeeui  8641  nosupcbv  27748  noinfcbv  27763  cbvriotavw2  36238  ellimciota  45634  fourierdlem96  46222  fourierdlem97  46223  fourierdlem98  46224  fourierdlem99  46225  fourierdlem105  46231  fourierdlem106  46232  fourierdlem108  46234  fourierdlem110  46236  fourierdlem112  46238  fourierdlem113  46239  fourierdlem115  46241  funressndmafv2rn  47240
  Copyright terms: Public domain W3C validator