Theorem cbvex 1805

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1509  ∃wex 1541

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

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

This theorem is referenced by:  sb8e  1906  cbvex2  1972  cbvmo  2120  mo23  2122  clelab  2360  cbvrexf  2769  issetf  2820  eqvincf  2941  rexab2  2982  cbvrexcsf  3201  abn0m  3533  rabn0m  3535  euabsn  3760  eluniab  3925  cbvopab1  4182  cbvopab2  4183  cbvopab1s  4184  intexabim  4263  iinexgm  4265  opeliunxp  4804  dfdmf  4948  dfrnf  4997  elrnmpt1  5007  cbvoprab1  6124  cbvoprab2  6125  opabex3d  6313  opabex3  6314  seq3f1olemp  10873  fsum2dlemstep  12113  bdsepnfALT  16646  strcollnfALT  16743