Theorem cbvex 1802

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1506  ∃wex 1538

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

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

This theorem is referenced by:  sb8e  1903  cbvex2  1969  cbvmo  2117  mo23  2119  clelab  2355  cbvrexf  2757  issetf  2808  eqvincf  2929  rexab2  2970  cbvrexcsf  3189  abn0m  3518  rabn0m  3520  euabsn  3739  eluniab  3903  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  intexabim  4240  iinexgm  4242  opeliunxp  4779  dfdmf  4922  dfrnf  4971  elrnmpt1  4981  cbvoprab1  6088  cbvoprab2  6089  opabex3d  6278  opabex3  6279  seq3f1olemp  10770  fsum2dlemstep  11988  bdsepnfALT  16434  strcollnfALT  16531