Theorem cbvrexw 3305

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

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

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 398  df-or 847  df-ex 1783  df-nf 1787  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072

This theorem is referenced by:  cbvrexsvw  3316  cbvrexsvwOLD  3318  cbvreuw  3407  cbvrmowOLD  3412  reu8nf  3872  cbviun  5040  isarep1  6638  isarep1OLD  6639  fvelimad  6960  elabrex  7242  onminex  7790  boxcutc  8935  indexfi  9360  wdom2d  9575  hsmexlem2  10422  fprodle  15940  iundisj  25065  mbfsup  25181  iundisjf  31820  iundisjfi  32007  voliune  33227  volfiniune  33228  bnj1542  33868  cvmcov  34254  poimirlem24  36512  poimirlem26  36514  indexa  36601  rexrabdioph  41532  rexfrabdioph  41533  elabrexg  43728  dffo3f  43877  disjrnmpt2  43886  caucvgbf  44200  limsuppnfd  44418  limsuppnf  44427  limsupre2  44441  limsupre3  44449  limsupre3uz  44452  limsupreuz  44453  liminfreuz  44519  stoweidlem31  44747  stoweidlem59  44775  rexsb  45807  cbvrex2  45812  2reu8i  45821