Theorem cbvexv 1906

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 1514	. 2 |- ( ph -> A. y ph )
2		ax-17 1514	. 2 |- ( ps -> A. x ps )
3		cbvalv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvexh 1743	1 |- ( E. x ph <-> E. y ps )

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

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eujust  2016  euind  2912  reuind  2930  r19.2m  3494  r19.3rm  3496  r19.9rmv  3499  raaanlem  3513  raaan  3514  cbvopab2v  4058  bm1.3ii  4102  mss  4203  zfun  4411  xpiindim  4740  relop  4753  dmmrnm  4822  dmxpm  4823  dmcoss  4872  xpm  5024  cnviinm  5144  fv3  5508  fo1stresm  6126  fo2ndresm  6127  tfr1onlemaccex  6312  tfrcllemaccex  6325  iinerm  6569  riinerm  6570  ixpiinm  6686  ac6sfi  6860  ctmlemr  7069  ctm  7070  ctssdclemr  7073  ctssdc  7074  fodjum  7106  acfun  7159  ccfunen  7201  cc2lem  7203  cc2  7204  ltexprlemdisj  7543  ltexprlemloc  7544  recexprlemdisj  7567  suplocsr  7746  axpre-suploc  7839  zfz1isolem1  10749  climmo  11235  summodc  11320  nninfdcex  11882  zsupssdc  11883  ctiunct  12369  neipsm  12754  suplociccex  13203  bdbm1.3ii  13733