Theorem cbvrexw 3276

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058

This theorem is referenced by:  cbvrexsvw  3285  cbvrexsvwOLD  3288  cbvreuw  3373  reu8nf  3824  cbviun  4985  isarep1  6575  fvelimad  6895  dffo3f  7045  elabrex  7182  elabrexg  7183  onminex  7741  boxcutc  8871  indexfi  9251  wdom2d  9473  hsmexlem2  10325  fprodle  15905  iundisj  25477  mbfsup  25593  iundisjf  32571  iundisjfi  32783  voliune  34263  volfiniune  34264  bnj1542  34890  cvmcov  35328  poimirlem24  37704  poimirlem26  37706  indexa  37793  mndmolinv  42208  primrootsunit1  42210  primrootsunit  42211  primrootspoweq0  42219  aks6d1c4  42237  aks6d1c6isolem1  42287  aks6d1c6isolem2  42288  rhmqusspan  42298  grpods  42307  unitscyglem1  42308  unitscyglem3  42310  unitscyglem4  42311  rexrabdioph  42911  rexfrabdioph  42912  disjrnmpt2  45309  caucvgbf  45611  limsuppnfd  45824  limsuppnf  45833  limsupre2  45847  limsupre3  45855  limsupre3uz  45858  limsupreuz  45859  liminfreuz  45925  stoweidlem31  46153  stoweidlem59  46181  rexsb  47223  cbvrex2  47228  2reu8i  47237