Theorem cbvrexw 3307

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-11 2191  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-nf 1813  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089

This theorem is used by:  cbvrexsvw  3316  cbvreuw  3394  reu8nf  3829  cbviun  4998  isarep1  6624  fvelimad  6948  dffo3f  7101  elabrex  7240  elabrexg  7241  onminex  7799  boxcutc  8937  indexfi  9315  wdom2d  9540  hsmexlem2  10417  fprodle  16057  iundisj  25718  mbfsup  25834  iundisjf  32945  iundisjfi  33152  voliune  34628  volfiniune  34629  bnj1542  35254  cvmcov  35763  poimirlem24  38323  poimirlem26  38325  indexa  38412  mndmolinv  42890  primrootsunit1  42892  primrootsunit  42893  primrootspoweq0  42901  aks6d1c4  42919  aks6d1c6isolem1  42969  aks6d1c6isolem2  42970  rhmqusspan  42980  grpods  42989  unitscyglem1  42990  unitscyglem3  42992  unitscyglem4  42993  rexrabdioph  43549  rexfrabdioph  43550  disjrnmpt2  45934  caucvgbf  46231  limsuppnfd  46444  limsuppnf  46453  limsupre2  46467  limsupre3  46475  limsupre3uz  46478  limsupreuz  46479  liminfreuz  46545  stoweidlem31  46773  stoweidlem59  46801  rexsb  47864  cbvrex2  47869  2reu8i  47878