Theorem cbvrexw 3283

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783  ∃wrex 3054

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 2804  df-nfc 2879  df-ral 3046  df-rex 3055

This theorem is referenced by:  cbvrexsvw  3293  cbvrexsvwOLD  3296  cbvreuw  3384  reu8nf  3843  cbviun  5003  isarep1  6609  isarep1OLD  6610  fvelimad  6931  dffo3f  7081  elabrex  7219  elabrexg  7220  onminex  7781  boxcutc  8917  indexfi  9318  wdom2d  9540  hsmexlem2  10387  fprodle  15969  iundisj  25456  mbfsup  25572  iundisjf  32525  iundisjfi  32726  voliune  34226  volfiniune  34227  bnj1542  34854  cvmcov  35257  poimirlem24  37645  poimirlem26  37647  indexa  37734  mndmolinv  42090  primrootsunit1  42092  primrootsunit  42093  primrootspoweq0  42101  aks6d1c4  42119  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  rhmqusspan  42180  grpods  42189  unitscyglem1  42190  unitscyglem3  42192  unitscyglem4  42193  rexrabdioph  42789  rexfrabdioph  42790  disjrnmpt2  45189  caucvgbf  45492  limsuppnfd  45707  limsuppnf  45716  limsupre2  45730  limsupre3  45738  limsupre3uz  45741  limsupreuz  45742  liminfreuz  45808  stoweidlem31  46036  stoweidlem59  46064  rexsb  47104  cbvrex2  47109  2reu8i  47118