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

Theorem cbvexv 2051
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
cbvalv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvexv  |-  ( E. x ph  <->  E. y ps )
Distinct variable groups:    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvexv
StepHypRef Expression
1 nfv 1728 . 2  |-  F/ y
ph
2 nfv 1728 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 2049 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1633
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
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638
This theorem is referenced by:  eujust  2240  euind  3235  reuind  3252  cbvopab2v  4468  bm1.3ii  4519  reusv2lem2  4595  relop  4973  dmcoss  5082  fv3  5861  exfo  6026  zfun  6574  wfrlem1  7019  ac6sfi  7797  brwdom2  8032  aceq1  8529  aceq0  8530  aceq3lem  8532  dfac4  8534  kmlem2  8562  kmlem13  8573  axdc4lem  8866  zfac  8871  zfcndun  9022  zfcndac  9026  sup2  10538  supmul  10550  climmo  13527  summo  13686  prodmo  13893  gsumval3eu  17229  elpt  20363  usgraedg4  24791  bnj1185  29166  frrlem1  30074  fdc  31500  axc11next  36141  fnchoice  36764
  Copyright terms: Public domain W3C validator