Theorem cbvrexw 3308

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1813  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090

This theorem is referenced by:  cbvrexsvw  3317  cbvreuw  3395  reu8nf  3831  cbviun  5000  isarep1  6626  fvelimad  6950  dffo3f  7103  elabrex  7242  elabrexg  7243  onminex  7802  boxcutc  8940  indexfi  9318  wdom2d  9543  hsmexlem2  10412  fprodle  16052  iundisj  25688  mbfsup  25804  iundisjf  32912  iundisjfi  33119  voliune  34597  volfiniune  34598  bnj1542  35223  cvmcov  35733  poimirlem24  38273  poimirlem26  38275  indexa  38362  mndmolinv  42840  primrootsunit1  42842  primrootsunit  42843  primrootspoweq0  42851  aks6d1c4  42869  aks6d1c6isolem1  42919  aks6d1c6isolem2  42920  rhmqusspan  42930  grpods  42939  unitscyglem1  42940  unitscyglem3  42942  unitscyglem4  42943  rexrabdioph  43501  rexfrabdioph  43502  disjrnmpt2  45886  caucvgbf  46183  limsuppnfd  46396  limsuppnf  46405  limsupre2  46419  limsupre3  46427  limsupre3uz  46430  limsupreuz  46431  liminfreuz  46497  stoweidlem31  46725  stoweidlem59  46753  rexsb  47813  cbvrex2  47818  2reu8i  47827