Theorem cbvex 2308

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 1824	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbval.2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1824	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbval.3	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 307	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbval 2307	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8	7	notbii 309	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9		df-ex 1745	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10		df-ex 1745	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
11	8, 9, 10	3bitr4i 292	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  ∀wal 1521  ∃wex 1744  Ⅎwnf 1748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750

This theorem is referenced by:  cbvexvOLD  2312  sb8e  2453  exsb  2496  euf  2506  mo2  2507  cbvmo  2535  clelab  2777  issetf  3239  eqvincf  3362  rexab2  3406  euabsn  4293  eluniab  4479  cbvopab1  4756  cbvopab2  4757  cbvopab1s  4758  axrep1  4805  axrep2  4806  axrep4  4808  opeliunxp  5204  dfdmf  5349  dfrnf  5396  elrnmpt1  5406  cbvoprab1  6769  cbvoprab2  6770  opabex3d  7187  opabex3  7188  zfcndrep  9474  fsum2dlem  14545  fprod2dlem  14754  bnj1146  30988  bnj607  31112  bnj1228  31205  poimirlem26  33565  sbcexf  34048  elunif  39489  stoweidlem46  40581  opeliun2xp  42436