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  7448  ctm  7449  ctssdclemr  7452  ctssdc  7453  fodjum  7486  finacn  7560  acfun  7563  ccfunen  7630  cc2lem  7632  cc2  7633  ltexprlemdisj  7973  ltexprlemloc  7974  recexprlemdisj  7997  suplocsr  8176  axpre-suploc  8269  nninfdcex  10672  zsupssdc  10673  zfz1isolem1  11292  climmo  12064  summodc  12150  nninfct  12818  ctiunct  13331  ismnd  13732  dfgrp3me  13905  issubg2m  13992  gsumvalfi  14152  subrgintm  14551  islssm  14694  islidlm  14816  neipsm  15255  suplociccex  15726  bdbm1.3ii  16917