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

Theorem cbviotavw 6504
Description: Change bound variables in a description binder. Version of cbviotav 6507 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by Gino Giotto, 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 2806 . . . . 5 {𝑥𝜑} = {𝑦𝜓}
32eqeq1i 2738 . . . 4 ({𝑥𝜑} = {𝑧} ↔ {𝑦𝜓} = {𝑧})
43abbii 2803 . . 3 {𝑧 ∣ {𝑥𝜑} = {𝑧}} = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
54unieqi 4922 . 2 {𝑧 ∣ {𝑥𝜑} = {𝑧}} = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
6 df-iota 6496 . 2 (℩𝑥𝜑) = {𝑧 ∣ {𝑥𝜑} = {𝑧}}
7 df-iota 6496 . 2 (℩𝑦𝜓) = {𝑧 ∣ {𝑦𝜓} = {𝑧}}
85, 6, 73eqtr4i 2771 1 (℩𝑥𝜑) = (℩𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  {cab 2710  {csn 4629   cuni 4909  cio 6494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-iota 6496
This theorem is referenced by:  cbvriotavw  7375  oeeui  8602  nosupcbv  27205  noinfcbv  27220  ellimciota  44330  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem105  44927  fourierdlem106  44928  fourierdlem108  44930  fourierdlem110  44932  fourierdlem112  44934  fourierdlem113  44935  fourierdlem115  44937  funressndmafv2rn  45931
  Copyright terms: Public domain W3C validator