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

Theorem cbvriotav 6576
Description: Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypothesis
Ref Expression
cbvriotav.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvriotav (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvriotav
StepHypRef Expression
1 nfv 1840 . 2 𝑦𝜑
2 nfv 1840 . 2 𝑥𝜓
3 cbvriotav.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvriota 6575 1 (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  crio 6564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-sn 4149  df-uni 4403  df-iota 5810  df-riota 6565
This theorem is referenced by:  ordtypecbv  8366  fin23lem27  9094  zorn2g  9269  uspgredg2v  26009  usgredg2v  26012  cnlnadji  28781  nmopadjlei  28793  cvmliftlem15  30985  cvmliftiota  30988  cvmlift2  31003  cvmlift3lem7  31012  cvmlift3  31015  lshpkrlem3  33876  cdleme40v  35234  lcfl7N  36267  lcf1o  36317  lcfrlem39  36347  hdmap1cbv  36569  wessf1ornlem  38842  fourierdlem103  39730  fourierdlem104  39731
  Copyright terms: Public domain W3C validator