Theorem cbvex 1743

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

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1447   E.wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521

This theorem depends on definitions:  df-bi 116  df-nf 1448

This theorem is referenced by:  sb8e  1844  cbvex2  1909  cbvmo  2053  mo23  2054  clelab  2290  cbvrexf  2683  issetf  2728  eqvincf  2846  rexab2  2887  cbvrexcsf  3103  abn0m  3429  rabn0m  3431  euabsn  3640  eluniab  3795  cbvopab1  4049  cbvopab2  4050  cbvopab1s  4051  intexabim  4125  iinexgm  4127  opeliunxp  4653  dfdmf  4791  dfrnf  4839  elrnmpt1  4849  cbvoprab1  5905  cbvoprab2  5906  opabex3d  6081  opabex3  6082  seq3f1olemp  10427  fsum2dlemstep  11361  bdsepnfALT  13606  strcollnfALT  13703