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

Theorem cbvriotavw 7118
 Description: Change bound variable in a restricted description binder. Version of cbvriotav 7122 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 26-Jan-2024.)
Hypothesis
Ref Expression
cbvriotavw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvriotavw (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvriotavw
StepHypRef Expression
1 nfv 1915 . 2 𝑦𝜑
2 nfv 1915 . 2 𝑥𝜓
3 cbvriotavw.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvriotaw 7117 1 (𝑥𝐴 𝜑) = (𝑦𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ℩crio 7107 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-sn 4523  df-uni 4799  df-iota 6294  df-riota 7108 This theorem is referenced by:  ordtypecbv  9014  fin23lem27  9788  zorn2g  9963  uspgredg2v  27113  usgredg2v  27116  cnlnadji  29958  nmopadjlei  29970  cvmliftlem15  32776  cvmliftiota  32779  cvmlift2  32794  cvmlift3lem7  32803  cvmlift3  32806  nosupcbv  33490  noinfcbv  33505  lshpkrlem3  36710  cdleme40v  38067  lcfl7N  39099  lcf1o  39149  lcfrlem39  39179  hdmap1cbv  39400  wessf1ornlem  42203  fourierdlem103  43239  fourierdlem104  43240
 Copyright terms: Public domain W3C validator