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 2371. (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 2892	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2892	. 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 1784  ∃wrex 3054

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 2112  ax-11 2159  ax-12 2179

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055

This theorem is referenced by:  cbvrexsvw  3282  cbvrexsvwOLD  3285  cbvreuw  3370  reu8nf  3826  cbviun  4983  isarep1  6566  fvelimad  6884  dffo3f  7034  elabrex  7171  elabrexg  7172  onminex  7730  boxcutc  8860  indexfi  9239  wdom2d  9461  hsmexlem2  10310  fprodle  15895  iundisj  25469  mbfsup  25585  iundisjf  32559  iundisjfi  32768  voliune  34232  volfiniune  34233  bnj1542  34859  cvmcov  35275  poimirlem24  37663  poimirlem26  37665  indexa  37752  mndmolinv  42107  primrootsunit1  42109  primrootsunit  42110  primrootspoweq0  42118  aks6d1c4  42136  aks6d1c6isolem1  42186  aks6d1c6isolem2  42187  rhmqusspan  42197  grpods  42206  unitscyglem1  42207  unitscyglem3  42209  unitscyglem4  42210  rexrabdioph  42806  rexfrabdioph  42807  disjrnmpt2  45204  caucvgbf  45506  limsuppnfd  45719  limsuppnf  45728  limsupre2  45742  limsupre3  45750  limsupre3uz  45753  limsupreuz  45754  liminfreuz  45820  stoweidlem31  46048  stoweidlem59  46076  rexsb  47109  cbvrex2  47114  2reu8i  47123