Theorem cbvex 2259

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
cbval.1	⊢ Ⅎ𝑦𝜑
cbval.2	⊢ Ⅎ𝑥𝜓
cbval.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvex	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbval.1	. . . . 5 ⊢ Ⅎ𝑦𝜑
2	1	nfn 1767	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbval.2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1767	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbval.3	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 306	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbval 2258	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8	7	notbii 308	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9		df-ex 1695	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10		df-ex 1695	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
11	8, 9, 10	3bitr4i 290	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 194  ∀wal 1472  ∃wex 1694  Ⅎwnf 1698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1700

This theorem is referenced by:  cbvexvOLD  2263  sb8e  2412  exsb  2455  euf  2465  mo2  2466  cbvmo  2493  clelab  2734  issetf  3180  eqvincf  3300  rexab2  3339  euabsn  4204  eluniab  4377  cbvopab1  4649  cbvopab2  4650  cbvopab1s  4651  axrep1  4694  axrep2  4695  axrep4  4697  opeliunxp  5082  dfdmf  5225  dfrnf  5271  elrnmpt1  5281  cbvoprab1  6602  cbvoprab2  6603  opabex3d  7014  opabex3  7015  zfcndrep  9292  fsum2dlem  14291  fprod2dlem  14497  bnj1146  29909  bnj607  30033  bnj1228  30126  poimirlem26  32388  sbcexf  32871  elunif  37981  stoweidlem46  38722  opeliun2xp  41885