Theorem cbvrexw 3373

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1790  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1787  df-nf 1791  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072

This theorem is referenced by:  cbvrmowOLD  3376  cbvrexsvw  3401  reu8nf  3815  cbviun  4971  isarep1  6520  fvelimad  6833  elabrex  7113  onminex  7646  boxcutc  8712  indexfi  9105  wdom2d  9317  hsmexlem2  10184  fprodle  15704  iundisj  24710  mbfsup  24826  iundisjf  30924  iundisjfi  31113  voliune  32193  volfiniune  32194  bnj1542  32833  cvmcov  33221  poimirlem24  35797  poimirlem26  35799  indexa  35887  rexrabdioph  40613  rexfrabdioph  40614  elabrexg  42559  dffo3f  42687  disjrnmpt2  42696  limsuppnfd  43214  limsuppnf  43223  limsupre2  43237  limsupre3  43245  limsupre3uz  43248  limsupreuz  43249  liminfreuz  43315  stoweidlem31  43543  stoweidlem59  43571  rexsb  44559  cbvrex2  44564  2reu8i  44573