Theorem cbvrex 3307

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	⊢ Ⅎ𝑦𝜑
cbvral.2	⊢ Ⅎ𝑥𝜓
cbvral.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrex	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvrex

Step	Hyp	Ref	Expression
1		nfcv 2902	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2902	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvral.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvral.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvral.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrexf 3305	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1857  ∃wrex 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056

This theorem is referenced by:  cbvrmo  3309  cbvrexv  3311  cbvrexsv  3322  reu8nf  3657  cbviun  4709  isarep1  6138  elabrex  6664  onminex  7172  boxcutc  8117  indexfi  8439  wdom2d  8650  hsmexlem2  9441  fprodle  14926  iundisj  23516  mbfsup  23630  iundisjf  29709  iundisjfi  29864  voliune  30601  volfiniune  30602  bnj1542  31234  cvmcov  31552  poimirlem24  33746  poimirlem26  33748  indexa  33841  rexrabdioph  37860  rexfrabdioph  37861  elabrexg  39705  dffo3f  39863  disjrnmpt2  39874  fvelimad  39957  limsuppnfd  40437  climinf2  40442  limsuppnf  40446  limsupre2  40460  limsupre3  40468  limsupre3uz  40471  limsupreuz  40472  liminfreuz  40538  stoweidlem31  40751  stoweidlem59  40779  meaiunincf  41203  rexsb  41674  cbvrex2  41679