Theorem cbvrexw 3375

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrex 3381 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 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 2908	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2908	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrexfw 3371	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1786  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071

This theorem is referenced by:  cbvreuw  3377  cbvrmowOLD  3379  cbvrexsvw  3404  reu8nf  3811  cbviun  4967  isarep1  6530  isarep1OLD  6531  fvelimad  6845  elabrex  7125  onminex  7661  boxcutc  8738  indexfi  9136  wdom2d  9348  hsmexlem2  10192  fprodle  15715  iundisj  24721  mbfsup  24837  iundisjf  30937  iundisjfi  31126  voliune  32206  volfiniune  32207  bnj1542  32846  cvmcov  33234  poimirlem24  35810  poimirlem26  35812  indexa  35900  rexrabdioph  40623  rexfrabdioph  40624  elabrexg  42596  dffo3f  42724  disjrnmpt2  42733  limsuppnfd  43250  limsuppnf  43259  limsupre2  43273  limsupre3  43281  limsupre3uz  43284  limsupreuz  43285  liminfreuz  43351  stoweidlem31  43579  stoweidlem59  43607  rexsb  44602  cbvrex2  44607  2reu8i  44616