Theorem cbvrexw 3313

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1781  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077

This theorem is referenced by:  cbvrexsvw  3324  cbvrexsvwOLD  3327  cbvreuw  3418  reu8nf  3899  cbviun  5059  isarep1  6667  isarep1OLD  6668  fvelimad  6989  dffo3f  7140  elabrex  7279  elabrexg  7280  onminex  7838  boxcutc  8999  indexfi  9430  wdom2d  9649  hsmexlem2  10496  fprodle  16044  iundisj  25602  mbfsup  25718  iundisjf  32611  iundisjfi  32801  voliune  34193  volfiniune  34194  bnj1542  34833  cvmcov  35231  poimirlem24  37604  poimirlem26  37606  indexa  37693  mndmolinv  42052  primrootsunit1  42054  primrootsunit  42055  primrootspoweq0  42063  aks6d1c4  42081  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  rhmqusspan  42142  grpods  42151  unitscyglem1  42152  unitscyglem3  42154  unitscyglem4  42155  rexrabdioph  42750  rexfrabdioph  42751  disjrnmpt2  45095  caucvgbf  45405  limsuppnfd  45623  limsuppnf  45632  limsupre2  45646  limsupre3  45654  limsupre3uz  45657  limsupreuz  45658  liminfreuz  45724  stoweidlem31  45952  stoweidlem59  45980  rexsb  47014  cbvrex2  47019  2reu8i  47028