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  2698  issetf  2745  eqvincf  2863  rexab2  2904  cbvrexcsf  3121  abn0m  3449  rabn0m  3451  euabsn  3663  eluniab  3822  cbvopab1  4077  cbvopab2  4078  cbvopab1s  4079  intexabim  4153  iinexgm  4155  opeliunxp  4682  dfdmf  4821  dfrnf  4869  elrnmpt1  4879  cbvoprab1  5947  cbvoprab2  5948  opabex3d  6122  opabex3  6123  seq3f1olemp  10502  fsum2dlemstep  11442  bdsepnfALT  14644  strcollnfALT  14741