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

Theorem cbvriotavw 7324
Description: Change bound variable in a restricted description binder. Version of cbvriotav 7329 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 30-Sep-2024.)
Hypothesis
Ref Expression
cbvriotavw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvriotavw (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvriotavw
StepHypRef Expression
1 eleq1w 2821 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvriotavw.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2anbi12d 632 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
43cbviotavw 6457 . 2 (℩𝑥(𝑥𝐴𝜑)) = (℩𝑦(𝑦𝐴𝜓))
5 df-riota 7314 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
6 df-riota 7314 . 2 (𝑦𝐴 𝜓) = (℩𝑦(𝑦𝐴𝜓))
74, 5, 63eqtr4i 2775 1 (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  cio 6447  crio 7313
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-uni 4867  df-iota 6449  df-riota 7314
This theorem is referenced by:  ordtypecbv  9454  fin23lem27  10265  zorn2g  10440  nosupcbv  27053  noinfcbv  27068  uspgredg2v  28175  usgredg2v  28178  cnlnadji  31021  nmopadjlei  31033  cvmliftlem15  33895  cvmliftiota  33898  cvmlift2  33913  cvmlift3lem7  33922  cvmlift3  33925  lshpkrlem3  37577  cdleme40v  38935  lcfl7N  39967  lcf1o  40017  lcfrlem39  40047  hdmap1cbv  40268  wessf1ornlem  43410  fourierdlem103  44457  fourierdlem104  44458
  Copyright terms: Public domain W3C validator