Theorem cbvrex 3168

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Hypotheses

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

Assertion

Ref	Expression
cbvrex	|- ( E. x e. A ph <-> E. y e. A ps )

Distinct variable groups:   x, A   y, A

Allowed substitution hints:   ph( x, y)   ps( x, y)

Proof of Theorem cbvrex

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 |- F/_ x A
2		nfcv 2764	. 2 |- F/_ y A
3		cbvral.1	. 2 |- F/ y ph
4		cbvral.2	. 2 |- F/ x ps
5		cbvral.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	1, 2, 3, 4, 5	cbvrexf 3166	1 |- ( E. x e. A ph <-> E. y e. A ps )

Syntax hints:   -> wi 4   <-> wb 196   F/wnf 1708   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918

This theorem is referenced by:  cbvrmo  3170  cbvrexv  3172  cbvrexsv  3183  reu8nf  3516  cbviun  4557  isarep1  5977  elabrex  6501  onminex  7007  boxcutc  7951  indexfi  8274  wdom2d  8485  hsmexlem2  9249  fprodle  14727  iundisj  23316  mbfsup  23431  iundisjf  29402  iundisjfi  29555  voliune  30292  volfiniune  30293  bnj1542  30927  cvmcov  31245  poimirlem24  33433  poimirlem26  33435  indexa  33528  rexrabdioph  37358  rexfrabdioph  37359  elabrexg  39206  dffo3f  39364  disjrnmpt2  39375  fvelimad  39458  limsuppnfd  39934  climinf2  39939  limsuppnf  39943  limsupre2  39957  limsupre3  39965  limsupre3uz  39968  limsupreuz  39969  liminfreuz  40035  stoweidlem31  40248  stoweidlem59  40276  rexsb  41168  cbvrex2  41173