Theorem cbvrexw 3295

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1778  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-11 2147  ax-12 2167

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-nf 1779  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061

This theorem is referenced by:  cbvrexsvw  3306  cbvrexsvwOLD  3308  cbvreuw  3394  reu8nf  3869  cbviun  5036  isarep1  6640  isarep1OLD  6641  fvelimad  6962  dffo3f  7112  elabrex  7249  elabrexg  7250  onminex  7803  boxcutc  8962  indexfi  9397  wdom2d  9616  hsmexlem2  10461  fprodle  15993  iundisj  25565  mbfsup  25681  iundisjf  32509  iundisjfi  32701  voliune  34075  volfiniune  34076  bnj1542  34715  cvmcov  35104  poimirlem24  37358  poimirlem26  37360  indexa  37447  mndmolinv  41807  primrootsunit1  41809  primrootsunit  41810  primrootspoweq0  41818  aks6d1c4  41836  aks6d1c6isolem1  41886  aks6d1c6isolem2  41887  rhmqusspan  41897  grpods  41906  unitscyglem1  41907  unitscyglem3  41909  unitscyglem4  41910  rexrabdioph  42488  rexfrabdioph  42489  disjrnmpt2  44831  caucvgbf  45141  limsuppnfd  45359  limsuppnf  45368  limsupre2  45382  limsupre3  45390  limsupre3uz  45393  limsupreuz  45394  liminfreuz  45460  stoweidlem31  45688  stoweidlem59  45716  rexsb  46748  cbvrex2  46753  2reu8i  46762