Theorem cbvrexw 3304

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

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1802  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-11 2190  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086

This theorem is referenced by:  cbvrexsvw  3313  cbvreuw  3392  reu8nf  3830  cbviun  4991  isarep1  6606  fvelimad  6930  dffo3f  7083  elabrex  7222  elabrexg  7223  onminex  7781  boxcutc  8919  indexfi  9300  wdom2d  9525  hsmexlem2  10381  fprodle  16009  iundisj  25590  mbfsup  25706  iundisjf  32738  iundisjfi  32948  voliune  34487  volfiniune  34488  bnj1542  35116  cvmcov  35577  poimirlem24  38107  poimirlem26  38109  indexa  38196  mndmolinv  42676  primrootsunit1  42678  primrootsunit  42679  primrootspoweq0  42687  aks6d1c4  42705  aks6d1c6isolem1  42755  aks6d1c6isolem2  42756  rhmqusspan  42766  grpods  42775  unitscyglem1  42776  unitscyglem3  42778  unitscyglem4  42779  rexrabdioph  43335  rexfrabdioph  43336  disjrnmpt2  45730  caucvgbf  46027  limsuppnfd  46240  limsuppnf  46249  limsupre2  46263  limsupre3  46271  limsupre3uz  46274  limsupreuz  46275  liminfreuz  46341  stoweidlem31  46569  stoweidlem59  46597  rexsb  47657  cbvrex2  47662  2reu8i  47671