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  4209  bm1.3ii  4256  mss  4368  zfun  4581  xpiindim  4919  relop  4932  reldmm  5002  dmmrnm  5003  dmxpm  5004  dmcoss  5054  xpm  5212  cnviinm  5332  iotam  5372  fv3  5721  elfvm  5732  mptmex  5948  fo1stresm  6399  fo2ndresm  6400  tfr1onlemaccex  6623  tfrcllemaccex  6636  iinerm  6885  riinerm  6886  ixpiinm  7010  ac6sfi  7206  ctmlemr  7454  ctm  7455  ctssdclemr  7458  ctssdc  7459  fodjum  7492  finacn  7566  acfun  7569  ccfunen  7636  cc2lem  7638  cc2  7639  ltexprlemdisj  7979  ltexprlemloc  7980  recexprlemdisj  8003  suplocsr  8182  axpre-suploc  8275  nninfdcex  10689  zsupssdc  10690  zfz1isolem1  11314  climmo  12089  summodc  12175  nninfct  12843  ctiunct  13389  ismnd  13791  dfgrp3me  13964  issubg2m  14051  gsumvalfi  14242  subrgintm  14660  islssm  14803  islidlm  14925  neipsm  15380  suplociccex  15851  bdbm1.3ii  17122