Theorem cbvexv 1918

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2028  euind  2924  reuind  2942  r19.2m  3509  r19.3rm  3511  r19.9rmv  3514  raaanlem  3528  raaan  3529  cbvopab2v  4080  bm1.3ii  4124  mss  4226  zfun  4434  xpiindim  4764  relop  4777  dmmrnm  4846  dmxpm  4847  dmcoss  4896  xpm  5050  cnviinm  5170  iotam  5208  fv3  5538  fo1stresm  6161  fo2ndresm  6162  tfr1onlemaccex  6348  tfrcllemaccex  6361  iinerm  6606  riinerm  6607  ixpiinm  6723  ac6sfi  6897  ctmlemr  7106  ctm  7107  ctssdclemr  7110  ctssdc  7111  fodjum  7143  acfun  7205  ccfunen  7262  cc2lem  7264  cc2  7265  ltexprlemdisj  7604  ltexprlemloc  7605  recexprlemdisj  7628  suplocsr  7807  axpre-suploc  7900  zfz1isolem1  10819  climmo  11305  summodc  11390  nninfdcex  11953  zsupssdc  11954  ctiunct  12440  ismnd  12819  dfgrp3me  12969  issubg2m  13047  subrgintm  13362  neipsm  13624  suplociccex  14073  bdbm1.3ii  14613