Theorem cbvrexw 3288

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3286 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.)

Hypotheses

Ref	Expression
cbvralw.1	⊢ Ⅎ𝑦𝜑
cbvralw.2	⊢ Ⅎ𝑥𝜓
cbvralw.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

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

Distinct variable group:   𝑥,𝑦,𝐴

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

Proof of Theorem cbvrexw

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1785  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070

This theorem is referenced by:  cbvrexsvw  3299  cbvreuw  3381  cbvrmowOLD  3386  reu8nf  3836  cbviun  5001  isarep1  6595  isarep1OLD  6596  fvelimad  6914  elabrex  7195  onminex  7742  boxcutc  8886  indexfi  9311  wdom2d  9525  hsmexlem2  10372  fprodle  15890  iundisj  24949  mbfsup  25065  iundisjf  31574  iundisjfi  31767  voliune  32917  volfiniune  32918  bnj1542  33558  cvmcov  33944  poimirlem24  36175  poimirlem26  36177  indexa  36265  rexrabdioph  41175  rexfrabdioph  41176  elabrexg  43371  dffo3f  43520  disjrnmpt2  43529  caucvgbf  43845  limsuppnfd  44063  limsuppnf  44072  limsupre2  44086  limsupre3  44094  limsupre3uz  44097  limsupreuz  44098  liminfreuz  44164  stoweidlem31  44392  stoweidlem59  44420  rexsb  45451  cbvrex2  45456  2reu8i  45465