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

Theorem cbvriotav 6084
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  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvriotav  |-  ( iota_ x  e.  A  ph )  =  ( iota_ y  e.  A  ps )
Distinct variable groups:    x, A    y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvriotav
StepHypRef Expression
1 nfv 1673 . 2  |-  F/ y
ph
2 nfv 1673 . 2  |-  F/ x ps
3 cbvriotav.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvriota 6083 1  |-  ( iota_ x  e.  A  ph )  =  ( iota_ y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   iota_crio 6072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742  df-sn 3899  df-uni 4113  df-iota 5402  df-riota 6073
This theorem is referenced by:  ordtypecbv  7752  fin23lem27  8518  zorn2g  8693  usgraidx2v  23333  cnlnadji  25502  nmopadjlei  25514  cvmliftlem15  27209  cvmliftiota  27212  cvmlift2  27227  cvmlift3lem7  27236  cvmlift3  27239  lshpkrlem3  32853  cdleme40v  34209  lcfl7N  35242  lcf1o  35292  lcfrlem39  35322  hdmap1cbv  35544
  Copyright terms: Public domain W3C validator