Theorem cbvrexw 3275

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057

This theorem is referenced by:  cbvrexsvw  3284  cbvrexsvwOLD  3287  cbvreuw  3372  reu8nf  3828  cbviun  4985  isarep1  6570  fvelimad  6889  dffo3f  7039  elabrex  7176  elabrexg  7177  onminex  7735  boxcutc  8865  indexfi  9244  wdom2d  9466  hsmexlem2  10315  fprodle  15900  iundisj  25474  mbfsup  25590  iundisjf  32564  iundisjfi  32773  voliune  34237  volfiniune  34238  bnj1542  34864  cvmcov  35295  poimirlem24  37683  poimirlem26  37685  indexa  37772  mndmolinv  42127  primrootsunit1  42129  primrootsunit  42130  primrootspoweq0  42138  aks6d1c4  42156  aks6d1c6isolem1  42206  aks6d1c6isolem2  42207  rhmqusspan  42217  grpods  42226  unitscyglem1  42227  unitscyglem3  42229  unitscyglem4  42230  rexrabdioph  42826  rexfrabdioph  42827  disjrnmpt2  45224  caucvgbf  45526  limsuppnfd  45739  limsuppnf  45748  limsupre2  45762  limsupre3  45770  limsupre3uz  45773  limsupreuz  45774  liminfreuz  45840  stoweidlem31  46068  stoweidlem59  46096  rexsb  47129  cbvrex2  47134  2reu8i  47143