Theorem cbvrexw 3305

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-11 2193  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087

This theorem is used by:  cbvrexsvw  3314  cbvreuw  3391  reu8nf  3823  cbviun  4992  isarep1  6628  fvelimad  6952  dffo3f  7106  elabrex  7246  elabrexg  7247  onminex  7816  boxcutc  8972  indexfi  9352  wdom2d  9577  hsmexlem2  10508  fprodle  16168  iundisj  25874  mbfsup  25990  iundisjf  33230  iundisjfi  33434  voliune  34908  volfiniune  34909  bnj1542  35533  cvmcov  36114  poimirlem24  38655  poimirlem26  38657  indexa  38760  mndmolinv  43238  primrootsunit1  43240  primrootsunit  43241  primrootspoweq0  43249  aks6d1c4  43267  aks6d1c6isolem1  43317  aks6d1c6isolem2  43318  rhmqusspan  43328  grpods  43337  unitscyglem1  43338  unitscyglem3  43340  unitscyglem4  43341  rexrabdioph  43894  rexfrabdioph  43895  disjrnmpt2  46296  caucvgbf  46592  limsuppnfd  46805  limsuppnf  46814  limsupre2  46828  limsupre3  46836  limsupre3uz  46839  limsupreuz  46840  liminfreuz  46906  stoweidlem31  47134  stoweidlem59  47162  rexsb  48262  cbvrex2  48267  2reu8i  48276