Theorem cbvexv 1967

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

Syntax hints:   -> wi 4   <-> wb 105   E.wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2081  euind  2993  reuind  3011  r19.2m  3581  r19.3rm  3583  r19.9rmv  3586  raaanlem  3599  raaan  3600  cbvopab2v  4166  bm1.3ii  4210  mss  4318  zfun  4531  xpiindim  4867  relop  4880  reldmm  4950  dmmrnm  4951  dmxpm  4952  dmcoss  5002  xpm  5158  cnviinm  5278  iotam  5318  fv3  5662  elfvm  5672  fo1stresm  6323  fo2ndresm  6324  tfr1onlemaccex  6513  tfrcllemaccex  6526  iinerm  6775  riinerm  6776  ixpiinm  6892  ac6sfi  7086  ctmlemr  7306  ctm  7307  ctssdclemr  7310  ctssdc  7311  fodjum  7344  finacn  7418  acfun  7421  ccfunen  7482  cc2lem  7484  cc2  7485  ltexprlemdisj  7825  ltexprlemloc  7826  recexprlemdisj  7849  suplocsr  8028  axpre-suploc  8121  nninfdcex  10496  zsupssdc  10497  zfz1isolem1  11103  climmo  11858  summodc  11943  nninfct  12611  ctiunct  13060  ismnd  13501  dfgrp3me  13682  issubg2m  13775  subrgintm  14256  islssm  14370  islidlm  14492  neipsm  14877  suplociccex  15348  bdbm1.3ii  16486  gfsumval  16680