Theorem cbvrexw 3283

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

Syntax hints:   → wi 4   ↔ wb 207  Ⅎwnf 1790  ∃wrex 3064

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 1974  ax-7 2015  ax-8 2121  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065

This theorem is referenced by:  cbvrexsvw  3292  cbvreuw  3371  reu8nf  3816  cbviun  4971  isarep1  6581  fvelimad  6901  dffo3f  7054  elabrex  7193  elabrexg  7194  onminex  7752  boxcutc  8886  indexfi  9267  wdom2d  9492  hsmexlem2  10347  fprodle  15959  iundisj  25540  mbfsup  25656  iundisjf  32685  iundisjfi  32895  voliune  34420  volfiniune  34421  bnj1542  35046  cvmcov  35498  poimirlem24  38018  poimirlem26  38020  indexa  38107  mndmolinv  42587  primrootsunit1  42589  primrootsunit  42590  primrootspoweq0  42598  aks6d1c4  42616  aks6d1c6isolem1  42666  aks6d1c6isolem2  42667  rhmqusspan  42677  grpods  42686  unitscyglem1  42687  unitscyglem3  42689  unitscyglem4  42690  rexrabdioph  43246  rexfrabdioph  43247  disjrnmpt2  45642  caucvgbf  45939  limsuppnfd  46152  limsuppnf  46161  limsupre2  46175  limsupre3  46183  limsupre3uz  46186  limsupreuz  46187  liminfreuz  46253  stoweidlem31  46481  stoweidlem59  46509  rexsb  47569  cbvrex2  47574  2reu8i  47583