Theorem cbvex 1805

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 1568	. 2 |- ( ph -> A. y ph )
3		cbvex.2	. . 3 |- F/ x ps
4	3	nfri 1568	. 2 |- ( ps -> A. x ps )
5		cbvex.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	2, 4, 5	cbvexh 1804	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1509   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  df-nf 1510

This theorem is referenced by:  sb8e  1906  cbvex2  1972  cbvmo  2120  mo23  2122  clelab  2360  cbvrexf  2770  issetf  2821  eqvincf  2942  rexab2  2983  cbvrexcsf  3202  abn0m  3534  rabn0m  3536  euabsn  3761  eluniab  3926  cbvopab1  4183  cbvopab2  4184  cbvopab1s  4185  intexabim  4264  iinexgm  4266  opeliunxp  4805  dfdmf  4949  dfrnf  4998  elrnmpt1  5008  cbvoprab1  6125  cbvoprab2  6126  opabex3d  6314  opabex3  6315  seq3f1olemp  10877  fsum2dlemstep  12120  bdsepnfALT  16659  strcollnfALT  16756