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  cbvreuw  3369  reu8nf  3816  cbviun  4978  isarep1  6581  fvelimad  6901  dffo3f  7052  elabrex  7190  elabrexg  7191  onminex  7749  boxcutc  8882  indexfi  9263  wdom2d  9488  hsmexlem2  10340  fprodle  15952  iundisj  25525  mbfsup  25641  iundisjf  32674  iundisjfi  32884  voliune  34389  volfiniune  34390  bnj1542  35015  cvmcov  35461  poimirlem24  37979  poimirlem26  37981  indexa  38068  mndmolinv  42548  primrootsunit1  42550  primrootsunit  42551  primrootspoweq0  42559  aks6d1c4  42577  aks6d1c6isolem1  42627  aks6d1c6isolem2  42628  rhmqusspan  42638  grpods  42647  unitscyglem1  42648  unitscyglem3  42650  unitscyglem4  42651  rexrabdioph  43240  rexfrabdioph  43241  disjrnmpt2  45636  caucvgbf  45935  limsuppnfd  46148  limsuppnf  46157  limsupre2  46171  limsupre3  46179  limsupre3uz  46182  limsupreuz  46183  liminfreuz  46249  stoweidlem31  46477  stoweidlem59  46505  rexsb  47559  cbvrex2  47564  2reu8i  47573