Theorem cbvexv 1967

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

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

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2081  euind  2994  reuind  3012  r19.2m  3583  r19.3rm  3585  r19.9rmv  3588  raaanlem  3601  raaan  3602  cbvopab2v  4171  bm1.3ii  4215  mss  4324  zfun  4537  xpiindim  4873  relop  4886  reldmm  4956  dmmrnm  4957  dmxpm  4958  dmcoss  5008  xpm  5165  cnviinm  5285  iotam  5325  fv3  5671  elfvm  5681  fo1stresm  6333  fo2ndresm  6334  tfr1onlemaccex  6557  tfrcllemaccex  6570  iinerm  6819  riinerm  6820  ixpiinm  6936  ac6sfi  7130  ctmlemr  7350  ctm  7351  ctssdclemr  7354  ctssdc  7355  fodjum  7388  finacn  7462  acfun  7465  ccfunen  7526  cc2lem  7528  cc2  7529  ltexprlemdisj  7869  ltexprlemloc  7870  recexprlemdisj  7893  suplocsr  8072  axpre-suploc  8165  nninfdcex  10543  zsupssdc  10544  zfz1isolem1  11150  climmo  11921  summodc  12007  nninfct  12675  ctiunct  13124  ismnd  13565  dfgrp3me  13746  issubg2m  13839  subrgintm  14321  islssm  14436  islidlm  14558  neipsm  14948  suplociccex  15419  bdbm1.3ii  16590  gfsumval  16792