Theorem cbvex 1803

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1508  ∃wex 1540

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

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

This theorem is referenced by:  sb8e  1904  cbvex2  1970  cbvmo  2118  mo23  2120  clelab  2356  cbvrexf  2758  issetf  2809  eqvincf  2930  rexab2  2971  cbvrexcsf  3190  abn0m  3519  rabn0m  3521  euabsn  3742  eluniab  3906  cbvopab1  4163  cbvopab2  4164  cbvopab1s  4165  intexabim  4243  iinexgm  4245  opeliunxp  4783  dfdmf  4926  dfrnf  4975  elrnmpt1  4985  cbvoprab1  6098  cbvoprab2  6099  opabex3d  6288  opabex3  6289  seq3f1olemp  10783  fsum2dlemstep  12018  bdsepnfALT  16544  strcollnfALT  16641