Theorem cbvex 1639

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
cbvex.1	|- F/ y ph
cbvex.2	|- F/ x ps
cbvex.3	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
cbvex	|- ( E. x ph <-> E. y ps )

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbvex.1	. . 3 |- F/ y ph
2	1	nfri 1412	. 2 |- ( ph -> A. y ph )
3		cbvex.2	. . 3 |- F/ x ps
4	3	nfri 1412	. 2 |- ( ps -> A. x ps )
5		cbvex.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	2, 4, 5	cbvexh 1638	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -> wi 4   <-> wb 98   F/wnf 1349   E.wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  sb8e  1737  cbvex2  1797  cbvmo  1940  mo23  1941  clelab  2162  cbvrexf  2528  issetf  2562  eqvincf  2669  rexab2  2707  cbvrexcsf  2909  rabn0m  3245  euabsn  3440  eluniab  3592  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  intexabim  3906  iinexgm  3908  opeliunxp  4395  dfdmf  4528  dfrnf  4575  elrnmpt1  4585  cbvoprab1  5576  cbvoprab2  5577  opabex3d  5748  opabex3  5749  bdsepnfALT  10009  strcollnfALT  10111