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 1816  ∃wrex 3088

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-11 2194  ax-12 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089

This theorem is used by:  cbvrexsvw  3316  cbvreuw  3393  reu8nf  3827  cbviun  4997  isarep1  6625  fvelimad  6949  dffo3f  7103  elabrex  7243  elabrexg  7244  onminex  7805  boxcutc  8952  indexfi  9331  wdom2d  9556  hsmexlem2  10433  fprodle  16089  iundisj  25782  mbfsup  25898  iundisjf  33070  iundisjfi  33275  voliune  34748  volfiniune  34749  bnj1542  35374  cvmcov  35850  poimirlem24  38401  poimirlem26  38403  indexa  38491  mndmolinv  42969  primrootsunit1  42971  primrootsunit  42972  primrootspoweq0  42980  aks6d1c4  42998  aks6d1c6isolem1  43048  aks6d1c6isolem2  43049  rhmqusspan  43059  grpods  43068  unitscyglem1  43069  unitscyglem3  43071  unitscyglem4  43072  rexrabdioph  43643  rexfrabdioph  43644  disjrnmpt2  46028  caucvgbf  46325  limsuppnfd  46538  limsuppnf  46547  limsupre2  46561  limsupre3  46569  limsupre3uz  46572  limsupreuz  46573  liminfreuz  46639  stoweidlem31  46867  stoweidlem59  46895  rexsb  47995  cbvrex2  48000  2reu8i  48009