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  6624  tfrcllemaccex  6637  iinerm  6886  riinerm  6887  ixpiinm  7012  ac6sfi  7208  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  10688  zsupssdc  10689  zfz1isolem1  11313  climmo  12088  summodc  12174  nninfct  12842  ctiunct  13388  ismnd  13790  dfgrp3me  13963  issubg2m  14050  gsumvalfi  14241  subrgintm  14659  islssm  14802  islidlm  14924  neipsm  15397  suplociccex  15868  bdbm1.3ii  17139