Theorem cbvexv 1891

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

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

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cbvexvw  1893  eujust  2002  euind  2875  reuind  2893  r19.2m  3454  r19.3rm  3456  r19.9rmv  3459  raaanlem  3473  raaan  3474  cbvopab2v  4013  bm1.3ii  4057  mss  4156  zfun  4364  xpiindim  4684  relop  4697  dmmrnm  4766  dmxpm  4767  dmcoss  4816  xpm  4968  cnviinm  5088  fv3  5452  fo1stresm  6067  fo2ndresm  6068  tfr1onlemaccex  6253  tfrcllemaccex  6266  iinerm  6509  riinerm  6510  ixpiinm  6626  ac6sfi  6800  ctmlemr  7001  ctm  7002  ctssdclemr  7005  ctssdc  7006  fodjum  7026  acfun  7080  ccfunen  7096  cc2lem  7098  cc2  7099  ltexprlemdisj  7438  ltexprlemloc  7439  recexprlemdisj  7462  suplocsr  7641  axpre-suploc  7734  zfz1isolem1  10615  climmo  11099  summodc  11184  ctiunct  11989  neipsm  12362  suplociccex  12811  bdbm1.3ii  13260