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

Theorem cbvriotavw 7374
Description: Change bound variable in a restricted description binder. Version of cbvriotav 7379 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 2816 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvriotavw.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2anbi12d 631 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
43cbviotavw 6503 . 2 (℩𝑥(𝑥𝐴𝜑)) = (℩𝑦(𝑦𝐴𝜓))
5 df-riota 7364 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
6 df-riota 7364 . 2 (𝑦𝐴 𝜓) = (℩𝑦(𝑦𝐴𝜓))
74, 5, 63eqtr4i 2770 1 (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  cio 6493  crio 7363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-iota 6495  df-riota 7364
This theorem is referenced by:  ordtypecbv  9511  fin23lem27  10322  zorn2g  10497  nosupcbv  27202  noinfcbv  27217  uspgredg2v  28478  usgredg2v  28481  cnlnadji  31324  nmopadjlei  31336  cvmliftlem15  34284  cvmliftiota  34287  cvmlift2  34302  cvmlift3lem7  34311  cvmlift3  34314  lshpkrlem3  37977  cdleme40v  39335  lcfl7N  40367  lcf1o  40417  lcfrlem39  40447  hdmap1cbv  40668  wessf1ornlem  43872  fourierdlem103  44915  fourierdlem104  44916
  Copyright terms: Public domain W3C validator