Theorem cbvex 1782

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1486  ∃wex 1518

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560

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

This theorem is referenced by:  sb8e  1883  cbvex2  1949  cbvmo  2097  mo23  2099  clelab  2335  cbvrexf  2737  issetf  2787  eqvincf  2908  rexab2  2949  cbvrexcsf  3168  abn0m  3497  rabn0m  3499  euabsn  3716  eluniab  3879  cbvopab1  4136  cbvopab2  4137  cbvopab1s  4138  intexabim  4215  iinexgm  4217  opeliunxp  4751  dfdmf  4893  dfrnf  4941  elrnmpt1  4951  cbvoprab1  6047  cbvoprab2  6048  opabex3d  6236  opabex3  6237  seq3f1olemp  10704  fsum2dlemstep  11911  bdsepnfALT  16162  strcollnfALT  16259