Theorem cbvex 1744

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
cbvex.1	⊢ Ⅎ𝑦𝜑
cbvex.2	⊢ Ⅎ𝑥𝜓
cbvex.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvex	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbvex.1	. . 3 ⊢ Ⅎ𝑦𝜑
2	1	nfri 1507	. 2 ⊢ (𝜑 → ∀𝑦𝜑)
3		cbvex.2	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	nfri 1507	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
5		cbvex.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	2, 4, 5	cbvexh 1743	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1448  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  sb8e  1845  cbvex2  1910  cbvmo  2054  mo23  2055  clelab  2292  cbvrexf  2686  issetf  2733  eqvincf  2851  rexab2  2892  cbvrexcsf  3108  abn0m  3434  rabn0m  3436  euabsn  3646  eluniab  3801  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  intexabim  4131  iinexgm  4133  opeliunxp  4659  dfdmf  4797  dfrnf  4845  elrnmpt1  4855  cbvoprab1  5914  cbvoprab2  5915  opabex3d  6089  opabex3  6090  seq3f1olemp  10437  fsum2dlemstep  11375  bdsepnfALT  13771  strcollnfALT  13868