Theorem cbvrexw 3273

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054

This theorem is referenced by:  cbvrexsvw  3282  cbvrexsvwOLD  3285  cbvreuw  3373  reu8nf  3831  cbviun  4988  isarep1  6575  fvelimad  6894  dffo3f  7044  elabrex  7182  elabrexg  7183  onminex  7742  boxcutc  8875  indexfi  9269  wdom2d  9491  hsmexlem2  10340  fprodle  15921  iundisj  25465  mbfsup  25581  iundisjf  32551  iundisjfi  32752  voliune  34195  volfiniune  34196  bnj1542  34823  cvmcov  35235  poimirlem24  37623  poimirlem26  37625  indexa  37712  mndmolinv  42068  primrootsunit1  42070  primrootsunit  42071  primrootspoweq0  42079  aks6d1c4  42097  aks6d1c6isolem1  42147  aks6d1c6isolem2  42148  rhmqusspan  42158  grpods  42167  unitscyglem1  42168  unitscyglem3  42170  unitscyglem4  42171  rexrabdioph  42767  rexfrabdioph  42768  disjrnmpt2  45166  caucvgbf  45469  limsuppnfd  45684  limsuppnf  45693  limsupre2  45707  limsupre3  45715  limsupre3uz  45718  limsupreuz  45719  liminfreuz  45785  stoweidlem31  46013  stoweidlem59  46041  rexsb  47084  cbvrex2  47089  2reu8i  47098