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 2377. (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 2905	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2905	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrexfw 3305	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071

This theorem is referenced by:  cbvrexsvw  3318  cbvrexsvwOLD  3321  cbvreuw  3410  reu8nf  3877  cbviun  5036  isarep1  6656  isarep1OLD  6657  fvelimad  6976  dffo3f  7126  elabrex  7262  elabrexg  7263  onminex  7822  boxcutc  8981  indexfi  9400  wdom2d  9620  hsmexlem2  10467  fprodle  16032  iundisj  25583  mbfsup  25699  iundisjf  32602  iundisjfi  32798  voliune  34230  volfiniune  34231  bnj1542  34871  cvmcov  35268  poimirlem24  37651  poimirlem26  37653  indexa  37740  mndmolinv  42096  primrootsunit1  42098  primrootsunit  42099  primrootspoweq0  42107  aks6d1c4  42125  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  rhmqusspan  42186  grpods  42195  unitscyglem1  42196  unitscyglem3  42198  unitscyglem4  42199  rexrabdioph  42805  rexfrabdioph  42806  disjrnmpt2  45193  caucvgbf  45500  limsuppnfd  45717  limsuppnf  45726  limsupre2  45740  limsupre3  45748  limsupre3uz  45751  limsupreuz  45752  liminfreuz  45818  stoweidlem31  46046  stoweidlem59  46074  rexsb  47111  cbvrex2  47116  2reu8i  47125