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

Theorem cbvriotavw 7398
Description: Change bound variable in a restricted description binder. Version of cbvriotav 7402 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by GG, 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 2824 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvriotavw.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2anbi12d 632 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
43cbviotavw 6522 . 2 (℩𝑥(𝑥𝐴𝜑)) = (℩𝑦(𝑦𝐴𝜓))
5 df-riota 7388 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
6 df-riota 7388 . 2 (𝑦𝐴 𝜓) = (℩𝑦(𝑦𝐴𝜓))
74, 5, 63eqtr4i 2775 1 (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  cio 6512  crio 7387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-iota 6514  df-riota 7388
This theorem is referenced by:  ordtypecbv  9557  fin23lem27  10368  zorn2g  10543  nosupcbv  27747  noinfcbv  27762  uspgredg2v  29241  usgredg2v  29244  cnlnadji  32095  nmopadjlei  32107  cvmliftlem15  35303  cvmliftiota  35306  cvmlift2  35321  cvmlift3lem7  35330  cvmlift3  35333  weiunlem2  36464  lshpkrlem3  39113  cdleme40v  40471  lcfl7N  41503  lcf1o  41553  lcfrlem39  41583  hdmap1cbv  41804  wessf1ornlem  45190  fourierdlem103  46224  fourierdlem104  46225
  Copyright terms: Public domain W3C validator