Theorem cbvex 1756

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

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

This theorem is referenced by:  sb8e  1857  cbvex2  1922  cbvmo  2066  mo23  2067  clelab  2303  cbvrexf  2698  issetf  2746  eqvincf  2864  rexab2  2905  cbvrexcsf  3122  abn0m  3450  rabn0m  3452  euabsn  3664  eluniab  3823  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  intexabim  4154  iinexgm  4156  opeliunxp  4683  dfdmf  4822  dfrnf  4870  elrnmpt1  4880  cbvoprab1  5949  cbvoprab2  5950  opabex3d  6124  opabex3  6125  seq3f1olemp  10504  fsum2dlemstep  11444  bdsepnfALT  14726  strcollnfALT  14823