Theorem cbvrexw 3309

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3307 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2404. (Revised by GG, 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 2926	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2926	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrexfw 3307	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091

This theorem is used by:  cbvrexsvw  3318  cbvreuw  3395  reu8nf  3828  cbviun  4996  isarep1  6650  fvelimad  6975  dffo3f  7130  elabrex  7269  elabrexg  7270  onminex  7840  boxcutc  8997  indexfi  9377  wdom2d  9601  hsmexlem2  10532  fprodle  16192  iundisj  25899  mbfsup  26015  iundisjf  33255  iundisjfi  33458  voliune  34932  volfiniune  34933  bnj1542  35557  cvmcov  36195  poimirlem24  38754  poimirlem26  38756  indexa  38859  mndmolinv  43337  primrootsunit1  43339  primrootsunit  43340  primrootspoweq0  43348  aks6d1c4  43366  aks6d1c6isolem1  43416  aks6d1c6isolem2  43417  rhmqusspan  43427  grpods  43436  unitscyglem1  43437  unitscyglem3  43439  unitscyglem4  43440  rexrabdioph  43994  rexfrabdioph  43995  disjrnmpt2  46408  caucvgbf  46704  limsuppnfd  46917  limsuppnf  46926  limsupre2  46940  limsupre3  46948  limsupre3uz  46951  limsupreuz  46952  liminfreuz  47018  stoweidlem31  47246  stoweidlem59  47274  rexsb  48375  cbvrex2  48380  2reu8i  48389