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 )

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

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 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 theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2088  euind  3013  reuind  3031  r19.2m  3611  r19.3rm  3613  r19.9rmv  3616  raaanlem  3629  raaan  3630  cbvopab2v  4203  bm1.3ii  4249  mss  4361  zfun  4574  xpiindim  4912  relop  4925  reldmm  4995  dmmrnm  4996  dmxpm  4997  dmcoss  5047  xpm  5204  cnviinm  5324  iotam  5364  fv3  5713  elfvm  5723  fo1stresm  6385  fo2ndresm  6386  tfr1onlemaccex  6609  tfrcllemaccex  6622  iinerm  6871  riinerm  6872  ixpiinm  6996  ac6sfi  7192  ctmlemr  7438  ctm  7439  ctssdclemr  7442  ctssdc  7443  fodjum  7476  finacn  7550  acfun  7553  ccfunen  7620  cc2lem  7622  cc2  7623  ltexprlemdisj  7963  ltexprlemloc  7964  recexprlemdisj  7987  suplocsr  8166  axpre-suploc  8259  nninfdcex  10650  zsupssdc  10651  zfz1isolem1  11270  climmo  12042  summodc  12128  nninfct  12796  ctiunct  13309  ismnd  13709  dfgrp3me  13882  issubg2m  13969  gsumvalfi  14129  subrgintm  14524  islssm  14666  islidlm  14788  neipsm  15178  suplociccex  15649  bdbm1.3ii  16831