Theorem cbvrexw 3306

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

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

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 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088

This theorem is used by:  cbvrexsvw  3315  cbvreuw  3392  reu8nf  3824  cbviun  4993  isarep1  6620  fvelimad  6944  dffo3f  7098  elabrex  7238  elabrexg  7239  onminex  7805  boxcutc  8953  indexfi  9333  wdom2d  9558  hsmexlem2  10486  fprodle  16143  iundisj  25849  mbfsup  25965  iundisjf  33165  iundisjfi  33370  voliune  34844  volfiniune  34845  bnj1542  35470  cvmcov  35997  poimirlem24  38530  poimirlem26  38532  indexa  38635  mndmolinv  43113  primrootsunit1  43115  primrootsunit  43116  primrootspoweq0  43124  aks6d1c4  43142  aks6d1c6isolem1  43192  aks6d1c6isolem2  43193  rhmqusspan  43203  grpods  43212  unitscyglem1  43213  unitscyglem3  43215  unitscyglem4  43216  rexrabdioph  43754  rexfrabdioph  43755  disjrnmpt2  46146  caucvgbf  46443  limsuppnfd  46656  limsuppnf  46665  limsupre2  46679  limsupre3  46687  limsupre3uz  46690  limsupreuz  46691  liminfreuz  46757  stoweidlem31  46985  stoweidlem59  47013  rexsb  48113  cbvrex2  48118  2reu8i  48127