Theorem cbvex 1767

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1471  ∃wex 1503

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

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

This theorem is referenced by:  sb8e  1868  cbvex2  1934  cbvmo  2082  mo23  2083  clelab  2319  cbvrexf  2719  issetf  2767  eqvincf  2885  rexab2  2926  cbvrexcsf  3144  abn0m  3472  rabn0m  3474  euabsn  3688  eluniab  3847  cbvopab1  4102  cbvopab2  4103  cbvopab1s  4104  intexabim  4181  iinexgm  4183  opeliunxp  4714  dfdmf  4855  dfrnf  4903  elrnmpt1  4913  cbvoprab1  5990  cbvoprab2  5991  opabex3d  6173  opabex3  6174  seq3f1olemp  10586  fsum2dlemstep  11577  bdsepnfALT  15381  strcollnfALT  15478