Theorem cbvex 1780

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1484  ∃wex 1516

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

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

This theorem is referenced by:  sb8e  1881  cbvex2  1947  cbvmo  2095  mo23  2096  clelab  2332  cbvrexf  2732  issetf  2780  eqvincf  2899  rexab2  2940  cbvrexcsf  3158  abn0m  3487  rabn0m  3489  euabsn  3704  eluniab  3864  cbvopab1  4121  cbvopab2  4122  cbvopab1s  4123  intexabim  4200  iinexgm  4202  opeliunxp  4734  dfdmf  4876  dfrnf  4924  elrnmpt1  4934  cbvoprab1  6024  cbvoprab2  6025  opabex3d  6213  opabex3  6214  seq3f1olemp  10667  fsum2dlemstep  11789  bdsepnfALT  15899  strcollnfALT  15996