Theorem cbvexv 1943

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2057  euind  2964  reuind  2982  r19.2m  3551  r19.3rm  3553  r19.9rmv  3556  raaanlem  3569  raaan  3570  cbvopab2v  4129  bm1.3ii  4173  mss  4278  zfun  4489  xpiindim  4823  relop  4836  dmmrnm  4906  dmxpm  4907  dmcoss  4957  xpm  5113  cnviinm  5233  iotam  5272  fv3  5612  elfvm  5622  fo1stresm  6260  fo2ndresm  6261  tfr1onlemaccex  6447  tfrcllemaccex  6460  iinerm  6707  riinerm  6708  ixpiinm  6824  ac6sfi  7010  ctmlemr  7225  ctm  7226  ctssdclemr  7229  ctssdc  7230  fodjum  7263  finacn  7332  acfun  7335  ccfunen  7396  cc2lem  7398  cc2  7399  ltexprlemdisj  7739  ltexprlemloc  7740  recexprlemdisj  7763  suplocsr  7942  axpre-suploc  8035  nninfdcex  10402  zsupssdc  10403  zfz1isolem1  11007  climmo  11684  summodc  11769  nninfct  12437  ctiunct  12886  ismnd  13326  dfgrp3me  13507  issubg2m  13600  subrgintm  14080  islssm  14194  islidlm  14316  neipsm  14701  suplociccex  15172  bdbm1.3ii  15965