Theorem cbvexv 1968

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

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

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2082  euind  3003  reuind  3021  r19.2m  3595  r19.3rm  3597  r19.9rmv  3600  raaanlem  3613  raaan  3614  cbvopab2v  4186  bm1.3ii  4230  mss  4341  zfun  4554  xpiindim  4891  relop  4904  reldmm  4974  dmmrnm  4975  dmxpm  4976  dmcoss  5026  xpm  5183  cnviinm  5303  iotam  5343  fv3  5692  elfvm  5702  fo1stresm  6354  fo2ndresm  6355  tfr1onlemaccex  6578  tfrcllemaccex  6591  iinerm  6840  riinerm  6841  ixpiinm  6958  ac6sfi  7154  ctmlemr  7398  ctm  7399  ctssdclemr  7402  ctssdc  7403  fodjum  7436  finacn  7510  acfun  7513  ccfunen  7577  cc2lem  7579  cc2  7580  ltexprlemdisj  7920  ltexprlemloc  7921  recexprlemdisj  7944  suplocsr  8123  axpre-suploc  8216  nninfdcex  10596  zsupssdc  10597  zfz1isolem1  11208  climmo  11979  summodc  12065  nninfct  12733  ctiunct  13183  ismnd  13624  dfgrp3me  13805  issubg2m  13898  subrgintm  14380  islssm  14497  islidlm  14619  neipsm  15011  suplociccex  15482  bdbm1.3ii  16653  gfsumval  16853