Theorem cbvex 1686

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

Syntax hints:   → wi 4   ↔ wb 103  Ⅎwnf 1394  ∃wex 1426

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472

This theorem depends on definitions:  df-bi 115  df-nf 1395

This theorem is referenced by:  sb8e  1785  cbvex2  1845  cbvmo  1988  mo23  1989  clelab  2212  cbvrexf  2585  issetf  2626  eqvincf  2742  rexab2  2781  cbvrexcsf  2991  abn0m  3308  rabn0m  3310  euabsn  3512  eluniab  3665  cbvopab1  3911  cbvopab2  3912  cbvopab1s  3913  intexabim  3988  iinexgm  3990  opeliunxp  4493  dfdmf  4629  dfrnf  4676  elrnmpt1  4686  cbvoprab1  5720  cbvoprab2  5721  opabex3d  5892  opabex3  5893  seq3f1olemp  9931  fsum2dlemstep  10828  bdsepnfALT  11780  strcollnfALT  11881