Theorem cbvrexw 3311

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

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

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 2148  ax-11 2195  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 2841  df-nfc 2915  df-ral 3083  df-rex 3093

This theorem is used by:  cbvrexsvw  3320  cbvreuw  3398  reu8nf  3833  cbviun  5004  isarep1  6631  fvelimad  6955  dffo3f  7108  elabrex  7247  elabrexg  7248  onminex  7810  boxcutc  8948  indexfi  9327  wdom2d  9552  hsmexlem2  10429  fprodle  16076  iundisj  25744  mbfsup  25860  iundisjf  32971  iundisjfi  33178  voliune  34651  volfiniune  34652  bnj1542  35277  cvmcov  35776  poimirlem24  38336  poimirlem26  38338  indexa  38425  mndmolinv  42903  primrootsunit1  42905  primrootsunit  42906  primrootspoweq0  42914  aks6d1c4  42932  aks6d1c6isolem1  42982  aks6d1c6isolem2  42983  rhmqusspan  42993  grpods  43002  unitscyglem1  43003  unitscyglem3  43005  unitscyglem4  43006  rexrabdioph  43562  rexfrabdioph  43563  disjrnmpt2  45947  caucvgbf  46244  limsuppnfd  46457  limsuppnf  46466  limsupre2  46480  limsupre3  46488  limsupre3uz  46491  limsupreuz  46492  liminfreuz  46558  stoweidlem31  46786  stoweidlem59  46814  rexsb  47877  cbvrex2  47882  2reu8i  47891