Theorem cbvex 1729

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 1499	. 2 ⊢ (𝜑 → ∀𝑦𝜑)
3		cbvex.2	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	nfri 1499	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
5		cbvex.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	2, 4, 5	cbvexh 1728	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1436  ∃wex 1468

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514

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

This theorem is referenced by:  sb8e  1829  cbvex2  1892  cbvmo  2037  mo23  2038  clelab  2263  cbvrexf  2647  issetf  2688  eqvincf  2805  rexab2  2845  cbvrexcsf  3058  abn0m  3383  rabn0m  3385  euabsn  3588  eluniab  3743  cbvopab1  3996  cbvopab2  3997  cbvopab1s  3998  intexabim  4072  iinexgm  4074  opeliunxp  4589  dfdmf  4727  dfrnf  4775  elrnmpt1  4785  cbvoprab1  5836  cbvoprab2  5837  opabex3d  6012  opabex3  6013  seq3f1olemp  10268  fsum2dlemstep  11196  bdsepnfALT  13076  strcollnfALT  13173