Theorem cbvex 1804

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1508  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509

This theorem is referenced by:  sb8e  1905  cbvex2  1971  cbvmo  2119  mo23  2121  clelab  2357  cbvrexf  2759  issetf  2810  eqvincf  2931  rexab2  2972  cbvrexcsf  3191  abn0m  3520  rabn0m  3522  euabsn  3741  eluniab  3905  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  intexabim  4242  iinexgm  4244  opeliunxp  4781  dfdmf  4924  dfrnf  4973  elrnmpt1  4983  cbvoprab1  6093  cbvoprab2  6094  opabex3d  6283  opabex3  6284  seq3f1olemp  10778  fsum2dlemstep  11997  bdsepnfALT  16505  strcollnfALT  16602