Theorem cbvrex 3373

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 2925	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2925	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvral.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvral.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvral.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrexf 3371	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 198  Ⅎwnf 1747  ∃wrex 3082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087

This theorem is referenced by:  cbvrmo  3375  cbvrexv  3377  cbvrexsv  3389  reu8nf  3756  cbviun  4827  isarep1  6272  fvelimad  6559  elabrex  6825  onminex  7336  boxcutc  8300  indexfi  8625  wdom2d  8837  hsmexlem2  9645  fprodle  15208  iundisj  23867  mbfsup  23983  iundisjf  30122  iundisjfi  30292  voliune  31165  volfiniune  31166  bnj1542  31808  cvmcov  32132  poimirlem24  34394  poimirlem26  34396  indexa  34487  rexrabdioph  38825  rexfrabdioph  38826  elabrexg  40760  dffo3f  40897  disjrnmpt2  40908  limsuppnfd  41448  climinf2  41453  limsuppnf  41457  limsupre2  41471  limsupre3  41479  limsupre3uz  41482  limsupreuz  41483  liminfreuz  41549  stoweidlem31  41781  stoweidlem59  41809  meaiunincf  42230  rexsb  42737  cbvrex2  42742  2reu8i  42752