Theorem cbvrexw 3279

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

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

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 2115  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061

This theorem is referenced by:  cbvrexsvw  3288  cbvrexsvwOLD  3291  cbvreuw  3376  reu8nf  3827  cbviun  4990  isarep1  6581  fvelimad  6901  dffo3f  7051  elabrex  7188  elabrexg  7189  onminex  7747  boxcutc  8879  indexfi  9260  wdom2d  9485  hsmexlem2  10337  fprodle  15919  iundisj  25505  mbfsup  25621  iundisjf  32664  iundisjfi  32876  voliune  34386  volfiniune  34387  bnj1542  35013  cvmcov  35457  poimirlem24  37841  poimirlem26  37843  indexa  37930  mndmolinv  42345  primrootsunit1  42347  primrootsunit  42348  primrootspoweq0  42356  aks6d1c4  42374  aks6d1c6isolem1  42424  aks6d1c6isolem2  42425  rhmqusspan  42435  grpods  42444  unitscyglem1  42445  unitscyglem3  42447  unitscyglem4  42448  rexrabdioph  43032  rexfrabdioph  43033  disjrnmpt2  45428  caucvgbf  45729  limsuppnfd  45942  limsuppnf  45951  limsupre2  45965  limsupre3  45973  limsupre3uz  45976  limsupreuz  45977  liminfreuz  46043  stoweidlem31  46271  stoweidlem59  46299  rexsb  47341  cbvrex2  47346  2reu8i  47355