Theorem cbvexv 1970

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  2084  euind  3007  reuind  3025  r19.2m  3600  r19.3rm  3602  r19.9rmv  3605  raaanlem  3618  raaan  3619  cbvopab2v  4192  bm1.3ii  4236  mss  4347  zfun  4560  xpiindim  4897  relop  4910  reldmm  4980  dmmrnm  4981  dmxpm  4982  dmcoss  5032  xpm  5189  cnviinm  5309  iotam  5349  fv3  5698  elfvm  5708  fo1stresm  6368  fo2ndresm  6369  tfr1onlemaccex  6592  tfrcllemaccex  6605  iinerm  6854  riinerm  6855  ixpiinm  6972  ac6sfi  7168  ctmlemr  7412  ctm  7413  ctssdclemr  7416  ctssdc  7417  fodjum  7450  finacn  7524  acfun  7527  ccfunen  7594  cc2lem  7596  cc2  7597  ltexprlemdisj  7937  ltexprlemloc  7938  recexprlemdisj  7961  suplocsr  8140  axpre-suploc  8233  nninfdcex  10621  zsupssdc  10622  zfz1isolem1  11237  climmo  12008  summodc  12094  nninfct  12762  ctiunct  13275  ismnd  13680  dfgrp3me  13855  issubg2m  13942  gfsumval  14102  subrgintm  14489  islssm  14631  islidlm  14753  neipsm  15145  suplociccex  15616  bdbm1.3ii  16787