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

Theorem cbvriotav 6251
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 1728 . 2  |-  F/ y
ph
2 nfv 1728 . 2  |-  F/ x ps
3 cbvriotav.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvriota 6250 1  |-  ( iota_ x  e.  A  ph )  =  ( iota_ y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1405   iota_crio 6239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2760  df-sn 3973  df-uni 4192  df-iota 5533  df-riota 6240
This theorem is referenced by:  ordtypecbv  7976  fin23lem27  8740  zorn2g  8915  usgraidx2v  24810  cnlnadji  27408  nmopadjlei  27420  cvmliftlem15  29595  cvmliftiota  29598  cvmlift2  29613  cvmlift3lem7  29622  cvmlift3  29625  lshpkrlem3  32130  cdleme40v  33488  lcfl7N  34521  lcf1o  34571  lcfrlem39  34601  hdmap1cbv  34823  fourierdlem103  37360  fourierdlem104  37361  usgedgvadf1  38044  usgedgvadf1ALT  38047
  Copyright terms: Public domain W3C validator