Theorem cbvrexw 3280

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3278 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 3278	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1785  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062

This theorem is referenced by:  cbvrexsvw  3289  cbvreuw  3368  reu8nf  3815  cbviun  4977  isarep1  6587  fvelimad  6907  dffo3f  7058  elabrex  7197  elabrexg  7198  onminex  7756  boxcutc  8889  indexfi  9270  wdom2d  9495  hsmexlem2  10349  fprodle  15961  iundisj  25515  mbfsup  25631  iundisjf  32659  iundisjfi  32869  voliune  34373  volfiniune  34374  bnj1542  34999  cvmcov  35445  poimirlem24  37965  poimirlem26  37967  indexa  38054  mndmolinv  42534  primrootsunit1  42536  primrootsunit  42537  primrootspoweq0  42545  aks6d1c4  42563  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  rhmqusspan  42624  grpods  42633  unitscyglem1  42634  unitscyglem3  42636  unitscyglem4  42637  rexrabdioph  43222  rexfrabdioph  43223  disjrnmpt2  45618  caucvgbf  45917  limsuppnfd  46130  limsuppnf  46139  limsupre2  46153  limsupre3  46161  limsupre3uz  46164  limsupreuz  46165  liminfreuz  46231  stoweidlem31  46459  stoweidlem59  46487  rexsb  47547  cbvrex2  47552  2reu8i  47561