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 2406. (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 2927	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2927	. 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 1806  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-11 2194  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-nf 1807  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090

This theorem is referenced by:  cbvrexsvw  3317  cbvreuw  3396  reu8nf  3833  cbviun  4995  isarep1  6614  fvelimad  6938  dffo3f  7091  elabrex  7230  elabrexg  7231  onminex  7789  boxcutc  8927  indexfi  9305  wdom2d  9530  hsmexlem2  10399  fprodle  16040  iundisj  25668  mbfsup  25784  iundisjf  32844  iundisjfi  33053  voliune  34536  volfiniune  34537  bnj1542  35162  cvmcov  35626  poimirlem24  38155  poimirlem26  38157  indexa  38244  mndmolinv  42724  primrootsunit1  42726  primrootsunit  42727  primrootspoweq0  42735  aks6d1c4  42753  aks6d1c6isolem1  42803  aks6d1c6isolem2  42804  rhmqusspan  42814  grpods  42823  unitscyglem1  42824  unitscyglem3  42826  unitscyglem4  42827  rexrabdioph  43383  rexfrabdioph  43384  disjrnmpt2  45764  caucvgbf  46061  limsuppnfd  46274  limsuppnf  46283  limsupre2  46297  limsupre3  46305  limsupre3uz  46308  limsupreuz  46309  liminfreuz  46375  stoweidlem31  46603  stoweidlem59  46631  rexsb  47691  cbvrex2  47696  2reu8i  47705