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

Theorem cbvriotavw 7377
Description: Change bound variable in a restricted description binder. Version of cbvriotav 7382 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 2814 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvriotavw.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2anbi12d 629 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
43cbviotavw 6502 . 2 (℩𝑥(𝑥𝐴𝜑)) = (℩𝑦(𝑦𝐴𝜓))
5 df-riota 7367 . 2 (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
6 df-riota 7367 . 2 (𝑦𝐴 𝜓) = (℩𝑦(𝑦𝐴𝜓))
74, 5, 63eqtr4i 2768 1 (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1539  wcel 2104  cio 6492  crio 7366
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-iota 6494  df-riota 7367
This theorem is referenced by:  ordtypecbv  9514  fin23lem27  10325  zorn2g  10500  nosupcbv  27441  noinfcbv  27456  uspgredg2v  28748  usgredg2v  28751  cnlnadji  31596  nmopadjlei  31608  cvmliftlem15  34587  cvmliftiota  34590  cvmlift2  34605  cvmlift3lem7  34614  cvmlift3  34617  lshpkrlem3  38285  cdleme40v  39643  lcfl7N  40675  lcf1o  40725  lcfrlem39  40755  hdmap1cbv  40976  wessf1ornlem  44182  fourierdlem103  45223  fourierdlem104  45224
  Copyright terms: Public domain W3C validator