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

Theorem cbvriotav 6894
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 1957 . 2 𝑦𝜑
2 nfv 1957 . 2 𝑥𝜓
3 cbvriotav.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvriota 6893 1 (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1601  crio 6882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-rex 3096  df-sn 4399  df-uni 4672  df-iota 6099  df-riota 6883
This theorem is referenced by:  ordtypecbv  8711  fin23lem27  9485  zorn2g  9660  uspgredg2v  26570  usgredg2v  26573  cnlnadji  29507  nmopadjlei  29519  cvmliftlem15  31879  cvmliftiota  31882  cvmlift2  31897  cvmlift3lem7  31906  cvmlift3  31909  lshpkrlem3  35268  cdleme40v  36625  lcfl7N  37657  lcf1o  37707  lcfrlem39  37737  hdmap1cbv  37958  wessf1ornlem  40298  fourierdlem103  41357  fourierdlem104  41358
  Copyright terms: Public domain W3C validator