Theorem cbvrexw 3287

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

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

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 848  df-ex 1780  df-nf 1784  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061

This theorem is referenced by:  cbvrexsvw  3297  cbvrexsvwOLD  3300  cbvreuw  3389  reu8nf  3852  cbviun  5012  isarep1  6626  isarep1OLD  6627  fvelimad  6946  dffo3f  7096  elabrex  7234  elabrexg  7235  onminex  7796  boxcutc  8955  indexfi  9372  wdom2d  9594  hsmexlem2  10441  fprodle  16012  iundisj  25501  mbfsup  25617  iundisjf  32570  iundisjfi  32773  voliune  34260  volfiniune  34261  bnj1542  34888  cvmcov  35285  poimirlem24  37668  poimirlem26  37670  indexa  37757  mndmolinv  42108  primrootsunit1  42110  primrootsunit  42111  primrootspoweq0  42119  aks6d1c4  42137  aks6d1c6isolem1  42187  aks6d1c6isolem2  42188  rhmqusspan  42198  grpods  42207  unitscyglem1  42208  unitscyglem3  42210  unitscyglem4  42211  rexrabdioph  42817  rexfrabdioph  42818  disjrnmpt2  45212  caucvgbf  45516  limsuppnfd  45731  limsuppnf  45740  limsupre2  45754  limsupre3  45762  limsupre3uz  45765  limsupreuz  45766  liminfreuz  45832  stoweidlem31  46060  stoweidlem59  46088  rexsb  47128  cbvrex2  47133  2reu8i  47142