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  3004  reuind  3022  r19.2m  3596  r19.3rm  3598  r19.9rmv  3601  raaanlem  3614  raaan  3615  cbvopab2v  4187  bm1.3ii  4231  mss  4342  zfun  4555  xpiindim  4892  relop  4905  reldmm  4975  dmmrnm  4976  dmxpm  4977  dmcoss  5027  xpm  5184  cnviinm  5304  iotam  5344  fv3  5693  elfvm  5703  fo1stresm  6355  fo2ndresm  6356  tfr1onlemaccex  6579  tfrcllemaccex  6592  iinerm  6841  riinerm  6842  ixpiinm  6959  ac6sfi  7155  ctmlemr  7399  ctm  7400  ctssdclemr  7403  ctssdc  7404  fodjum  7437  finacn  7511  acfun  7514  ccfunen  7578  cc2lem  7580  cc2  7581  ltexprlemdisj  7921  ltexprlemloc  7922  recexprlemdisj  7945  suplocsr  8124  axpre-suploc  8217  nninfdcex  10597  zsupssdc  10598  zfz1isolem1  11212  climmo  11983  summodc  12069  nninfct  12737  ctiunct  13191  ismnd  13632  dfgrp3me  13813  issubg2m  13906  subrgintm  14388  islssm  14505  islidlm  14627  neipsm  15019  suplociccex  15490  bdbm1.3ii  16661  gfsumval  16862