Theorem cbvex 1730

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

Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1437  ∃wex 1469

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515

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

This theorem is referenced by:  sb8e  1830  cbvex2  1895  cbvmo  2040  mo23  2041  clelab  2266  cbvrexf  2652  issetf  2696  eqvincf  2814  rexab2  2854  cbvrexcsf  3068  abn0m  3393  rabn0m  3395  euabsn  3601  eluniab  3756  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  intexabim  4085  iinexgm  4087  opeliunxp  4602  dfdmf  4740  dfrnf  4788  elrnmpt1  4798  cbvoprab1  5851  cbvoprab2  5852  opabex3d  6027  opabex3  6028  seq3f1olemp  10306  fsum2dlemstep  11235  bdsepnfALT  13258  strcollnfALT  13355