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

Theorem cbvriotav 6268
 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:   ,   ,   ,   ,

Proof of Theorem cbvriotav
StepHypRef Expression
1 nfv 1707 . 2
2 nfv 1707 . 2
3 cbvriotav.1 . 2
41, 2, 3cbvriota 6267 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  iota_crio 6256 This theorem is referenced by:  ordtypecbv  7963  fin23lem27  8729  zorn2g  8904  usgraidx2v  24393  cnlnadji  26995  nmopadjlei  27007  cvmliftlem15  28743  cvmliftiota  28746  cvmlift2  28761  cvmlift3lem7  28770  cvmlift3  28773  fourierdlem103  31992  fourierdlem104  31993  usgedgvadf1  32415  usgedgvadf1ALT  32418  lshpkrlem3  34837  cdleme40v  36195  lcfl7N  37228  lcf1o  37278  lcfrlem39  37308  hdmap1cbv  37530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-sn 4030  df-uni 4250  df-iota 5556  df-riota 6257
 Copyright terms: Public domain W3C validator