Theorem cbvexv 1890

Description: Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-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

Step	Hyp	Ref	Expression
1		ax-17 1506	. 2 |- ( ph -> A. y ph )
2		ax-17 1506	. 2 |- ( ps -> A. x ps )
3		cbvalv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvexh 1728	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -> wi 4   <-> wb 104   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eujust  1999  euind  2866  reuind  2884  r19.2m  3444  r19.3rm  3446  r19.9rmv  3449  raaanlem  3463  raaan  3464  cbvopab2v  4000  bm1.3ii  4044  mss  4143  zfun  4351  xpiindim  4671  relop  4684  dmmrnm  4753  dmxpm  4754  dmcoss  4803  xpm  4955  cnviinm  5075  fv3  5437  fo1stresm  6052  fo2ndresm  6053  tfr1onlemaccex  6238  tfrcllemaccex  6251  iinerm  6494  riinerm  6495  ixpiinm  6611  ac6sfi  6785  ctmlemr  6986  ctm  6987  ctssdclemr  6990  ctssdc  6991  fodjum  7011  acfun  7056  ccfunen  7072  ltexprlemdisj  7407  ltexprlemloc  7408  recexprlemdisj  7431  suplocsr  7610  axpre-suploc  7703  zfz1isolem1  10576  climmo  11060  summodc  11145  ctiunct  11942  neipsm  12312  suplociccex  12761  bdbm1.3ii  13078