Theorem cbvexv 1911

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

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

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eujust  2021  euind  2917  reuind  2935  r19.2m  3501  r19.3rm  3503  r19.9rmv  3506  raaanlem  3520  raaan  3521  cbvopab2v  4066  bm1.3ii  4110  mss  4211  zfun  4419  xpiindim  4748  relop  4761  dmmrnm  4830  dmxpm  4831  dmcoss  4880  xpm  5032  cnviinm  5152  iotam  5190  fv3  5519  fo1stresm  6140  fo2ndresm  6141  tfr1onlemaccex  6327  tfrcllemaccex  6340  iinerm  6585  riinerm  6586  ixpiinm  6702  ac6sfi  6876  ctmlemr  7085  ctm  7086  ctssdclemr  7089  ctssdc  7090  fodjum  7122  acfun  7184  ccfunen  7226  cc2lem  7228  cc2  7229  ltexprlemdisj  7568  ltexprlemloc  7569  recexprlemdisj  7592  suplocsr  7771  axpre-suploc  7864  zfz1isolem1  10775  climmo  11261  summodc  11346  nninfdcex  11908  zsupssdc  11909  ctiunct  12395  ismnd  12655  neipsm  12948  suplociccex  13397  bdbm1.3ii  13926