Theorem cbvexv 1974

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  eujust  2088  euind  3013  reuind  3031  r19.2m  3614  r19.3rm  3616  r19.9rmv  3619  raaanlem  3632  raaan  3633  cbvopab2v  4208  bm1.3ii  4254  mss  4366  zfun  4579  xpiindim  4917  relop  4930  reldmm  5000  dmmrnm  5001  dmxpm  5002  dmcoss  5052  xpm  5209  cnviinm  5329  iotam  5369  fv3  5718  elfvm  5729  mptmex  5945  fo1stresm  6395  fo2ndresm  6396  tfr1onlemaccex  6619  tfrcllemaccex  6632  iinerm  6881  riinerm  6882  ixpiinm  7006  ac6sfi  7202  ctmlemr  7449  ctm  7450  ctssdclemr  7453  ctssdc  7454  fodjum  7487  finacn  7561  acfun  7564  ccfunen  7631  cc2lem  7633  cc2  7634  ltexprlemdisj  7974  ltexprlemloc  7975  recexprlemdisj  7998  suplocsr  8177  axpre-suploc  8270  nninfdcex  10683  zsupssdc  10684  zfz1isolem1  11308  climmo  12083  summodc  12169  nninfct  12837  ctiunct  13383  ismnd  13785  dfgrp3me  13958  issubg2m  14045  gsumvalfi  14236  subrgintm  14635  islssm  14778  islidlm  14900  neipsm  15346  suplociccex  15817  bdbm1.3ii  17083