Theorem cbvexv 1965

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

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

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2079  euind  2991  reuind  3009  r19.2m  3579  r19.3rm  3581  r19.9rmv  3584  raaanlem  3597  raaan  3598  cbvopab2v  4164  bm1.3ii  4208  mss  4316  zfun  4529  xpiindim  4865  relop  4878  reldmm  4948  dmmrnm  4949  dmxpm  4950  dmcoss  5000  xpm  5156  cnviinm  5276  iotam  5316  fv3  5658  elfvm  5668  fo1stresm  6319  fo2ndresm  6320  tfr1onlemaccex  6509  tfrcllemaccex  6522  iinerm  6771  riinerm  6772  ixpiinm  6888  ac6sfi  7080  ctmlemr  7298  ctm  7299  ctssdclemr  7302  ctssdc  7303  fodjum  7336  finacn  7409  acfun  7412  ccfunen  7473  cc2lem  7475  cc2  7476  ltexprlemdisj  7816  ltexprlemloc  7817  recexprlemdisj  7840  suplocsr  8019  axpre-suploc  8112  nninfdcex  10487  zsupssdc  10488  zfz1isolem1  11094  climmo  11849  summodc  11934  nninfct  12602  ctiunct  13051  ismnd  13492  dfgrp3me  13673  issubg2m  13766  subrgintm  14247  islssm  14361  islidlm  14483  neipsm  14868  suplociccex  15339  bdbm1.3ii  16422