Theorem cbvrexw 3281

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

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

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 2812  df-nfc 2886  df-ral 3053  df-rex 3063

This theorem is referenced by:  cbvrexsvw  3290  cbvrexsvwOLD  3293  cbvreuw  3378  reu8nf  3829  cbviun  4992  isarep1  6589  fvelimad  6909  dffo3f  7060  elabrex  7198  elabrexg  7199  onminex  7757  boxcutc  8891  indexfi  9272  wdom2d  9497  hsmexlem2  10349  fprodle  15931  iundisj  25517  mbfsup  25633  iundisjf  32675  iundisjfi  32886  voliune  34406  volfiniune  34407  bnj1542  35032  cvmcov  35476  poimirlem24  37889  poimirlem26  37891  indexa  37978  mndmolinv  42459  primrootsunit1  42461  primrootsunit  42462  primrootspoweq0  42470  aks6d1c4  42488  aks6d1c6isolem1  42538  aks6d1c6isolem2  42539  rhmqusspan  42549  grpods  42558  unitscyglem1  42559  unitscyglem3  42561  unitscyglem4  42562  rexrabdioph  43145  rexfrabdioph  43146  disjrnmpt2  45541  caucvgbf  45841  limsuppnfd  46054  limsuppnf  46063  limsupre2  46077  limsupre3  46085  limsupre3uz  46088  limsupreuz  46089  liminfreuz  46155  stoweidlem31  46383  stoweidlem59  46411  rexsb  47453  cbvrex2  47458  2reu8i  47467