Theorem cbvex 1736

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

Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1440  ∃wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1441

This theorem is referenced by:  sb8e  1837  cbvex2  1902  cbvmo  2046  mo23  2047  clelab  2283  cbvrexf  2675  issetf  2719  eqvincf  2837  rexab2  2878  cbvrexcsf  3094  abn0m  3419  rabn0m  3421  euabsn  3629  eluniab  3784  cbvopab1  4037  cbvopab2  4038  cbvopab1s  4039  intexabim  4113  iinexgm  4115  opeliunxp  4641  dfdmf  4779  dfrnf  4827  elrnmpt1  4837  cbvoprab1  5893  cbvoprab2  5894  opabex3d  6069  opabex3  6070  seq3f1olemp  10401  fsum2dlemstep  11331  bdsepnfALT  13475  strcollnfALT  13572