Theorem cbvrexw 3388

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1785  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112

This theorem is referenced by:  cbvrmowOLD  3391  cbvrexsvw  3415  reu8nf  3806  cbviun  4923  isarep1  6412  fvelimad  6707  elabrex  6980  onminex  7502  boxcutc  8488  indexfi  8816  wdom2d  9028  hsmexlem2  9838  fprodle  15342  iundisj  24152  mbfsup  24268  iundisjf  30352  iundisjfi  30545  voliune  31598  volfiniune  31599  bnj1542  32239  cvmcov  32623  poimirlem24  35081  poimirlem26  35083  indexa  35171  rexrabdioph  39735  rexfrabdioph  39736  elabrexg  41675  dffo3f  41806  disjrnmpt2  41815  limsuppnfd  42344  limsuppnf  42353  limsupre2  42367  limsupre3  42375  limsupre3uz  42378  limsupreuz  42379  liminfreuz  42445  stoweidlem31  42673  stoweidlem59  42701  rexsb  43654  cbvrex2  43659  2reu8i  43669