Theorem cbvrexw 3442

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrex 3446 with a disjoint variable condition, which does not require ax-13 2390. (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 2977	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2977	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrexfw 3438	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1784  ∃wrex 3139

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 1970  ax-7 2015  ax-8 2116  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144

This theorem is referenced by:  cbvrmow  3444  cbvrexsvw  3468  reu8nf  3860  cbviun  4961  isarep1  6442  fvelimad  6732  elabrex  7002  onminex  7522  boxcutc  8505  indexfi  8832  wdom2d  9044  hsmexlem2  9849  fprodle  15350  iundisj  24149  mbfsup  24265  iundisjf  30339  iundisjfi  30519  voliune  31488  volfiniune  31489  bnj1542  32129  cvmcov  32510  poimirlem24  34931  poimirlem26  34933  indexa  35023  rexrabdioph  39440  rexfrabdioph  39441  elabrexg  41352  dffo3f  41487  disjrnmpt2  41498  limsuppnfd  42032  limsuppnf  42041  limsupre2  42055  limsupre3  42063  limsupre3uz  42066  limsupreuz  42067  liminfreuz  42133  stoweidlem31  42365  stoweidlem59  42393  rexsb  43346  2reu8i  43361