Theorem cbvrex 3317

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

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1856  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067

This theorem is referenced by:  cbvrmo  3319  cbvrexv  3321  cbvrexsv  3332  reu8nf  3665  cbviun  4691  isarep1  6117  elabrex  6644  onminex  7154  boxcutc  8105  indexfi  8430  wdom2d  8641  hsmexlem2  9451  fprodle  14933  iundisj  23536  mbfsup  23651  iundisjf  29740  iundisjfi  29895  voliune  30632  volfiniune  30633  bnj1542  31265  cvmcov  31583  poimirlem24  33766  poimirlem26  33768  indexa  33860  rexrabdioph  37884  rexfrabdioph  37885  elabrexg  39728  dffo3f  39884  disjrnmpt2  39895  fvelimad  39976  limsuppnfd  40452  climinf2  40457  limsuppnf  40461  limsupre2  40475  limsupre3  40483  limsupre3uz  40486  limsupreuz  40487  liminfreuz  40553  stoweidlem31  40765  stoweidlem59  40793  meaiunincf  41217  rexsb  41688  cbvrex2  41693