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 2370. (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 2891	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2891	. 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 1783  ∃wrex 3053

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 2008  ax-8 2111  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054

This theorem is referenced by:  cbvrexsvw  3291  cbvrexsvwOLD  3294  cbvreuw  3382  reu8nf  3840  cbviun  5000  isarep1  6606  isarep1OLD  6607  fvelimad  6928  dffo3f  7078  elabrex  7216  elabrexg  7217  onminex  7778  boxcutc  8914  indexfi  9311  wdom2d  9533  hsmexlem2  10380  fprodle  15962  iundisj  25449  mbfsup  25565  iundisjf  32518  iundisjfi  32719  voliune  34219  volfiniune  34220  bnj1542  34847  cvmcov  35250  poimirlem24  37638  poimirlem26  37640  indexa  37727  mndmolinv  42083  primrootsunit1  42085  primrootsunit  42086  primrootspoweq0  42094  aks6d1c4  42112  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  rhmqusspan  42173  grpods  42182  unitscyglem1  42183  unitscyglem3  42185  unitscyglem4  42186  rexrabdioph  42782  rexfrabdioph  42783  disjrnmpt2  45182  caucvgbf  45485  limsuppnfd  45700  limsuppnf  45709  limsupre2  45723  limsupre3  45731  limsupre3uz  45734  limsupreuz  45735  liminfreuz  45801  stoweidlem31  46029  stoweidlem59  46057  rexsb  47100  cbvrex2  47105  2reu8i  47114