Theorem cbvrexw 3364

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1787  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069

This theorem is referenced by:  cbvrmowOLD  3367  cbvrexsvw  3392  reu8nf  3806  cbviun  4962  isarep1  6506  fvelimad  6818  elabrex  7098  onminex  7629  boxcutc  8687  indexfi  9057  wdom2d  9269  hsmexlem2  10114  fprodle  15634  iundisj  24617  mbfsup  24733  iundisjf  30829  iundisjfi  31019  voliune  32097  volfiniune  32098  bnj1542  32737  cvmcov  33125  poimirlem24  35728  poimirlem26  35730  indexa  35818  rexrabdioph  40532  rexfrabdioph  40533  elabrexg  42478  dffo3f  42606  disjrnmpt2  42615  limsuppnfd  43133  limsuppnf  43142  limsupre2  43156  limsupre3  43164  limsupre3uz  43167  limsupreuz  43168  liminfreuz  43234  stoweidlem31  43462  stoweidlem59  43490  rexsb  44478  cbvrex2  44483  2reu8i  44492