Theorem cbvexv 1933

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2047  euind  2951  reuind  2969  r19.2m  3538  r19.3rm  3540  r19.9rmv  3543  raaanlem  3556  raaan  3557  cbvopab2v  4111  bm1.3ii  4155  mss  4260  zfun  4470  xpiindim  4804  relop  4817  dmmrnm  4886  dmxpm  4887  dmcoss  4936  xpm  5092  cnviinm  5212  iotam  5251  fv3  5584  elfvm  5594  fo1stresm  6228  fo2ndresm  6229  tfr1onlemaccex  6415  tfrcllemaccex  6428  iinerm  6675  riinerm  6676  ixpiinm  6792  ac6sfi  6968  ctmlemr  7183  ctm  7184  ctssdclemr  7187  ctssdc  7188  fodjum  7221  finacn  7287  acfun  7290  ccfunen  7347  cc2lem  7349  cc2  7350  ltexprlemdisj  7690  ltexprlemloc  7691  recexprlemdisj  7714  suplocsr  7893  axpre-suploc  7986  nninfdcex  10344  zsupssdc  10345  zfz1isolem1  10949  climmo  11480  summodc  11565  nninfct  12233  ctiunct  12682  ismnd  13121  dfgrp3me  13302  issubg2m  13395  subrgintm  13875  islssm  13989  islidlm  14111  neipsm  14474  suplociccex  14945  bdbm1.3ii  15621