Theorem cbvex 1756

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1460  ∃wex 1492

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

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

This theorem is referenced by:  sb8e  1857  cbvex2  1922  cbvmo  2066  mo23  2067  clelab  2303  cbvrexf  2697  issetf  2744  eqvincf  2862  rexab2  2903  cbvrexcsf  3120  abn0m  3448  rabn0m  3450  euabsn  3662  eluniab  3821  cbvopab1  4076  cbvopab2  4077  cbvopab1s  4078  intexabim  4152  iinexgm  4154  opeliunxp  4681  dfdmf  4820  dfrnf  4868  elrnmpt1  4878  cbvoprab1  5946  cbvoprab2  5947  opabex3d  6121  opabex3  6122  seq3f1olemp  10501  fsum2dlemstep  11441  bdsepnfALT  14577  strcollnfALT  14674