Theorem cbvex 1985

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

Hypotheses

Ref	Expression
cbvex.1	⊢ Ⅎyφ
cbvex.2	⊢ Ⅎxψ
cbvex.3	⊢ (x = y → (φ ↔ ψ))

Assertion

Ref	Expression
cbvex	⊢ (∃xφ ↔ ∃yψ)

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbvex.1	. . . . 5 ⊢ Ⅎyφ
2	1	nfn 1793	. . . 4 ⊢ Ⅎy ¬ φ
3		cbvex.2	. . . . 5 ⊢ Ⅎxψ
4	3	nfn 1793	. . . 4 ⊢ Ⅎx ¬ ψ
5		cbvex.3	. . . . 5 ⊢ (x = y → (φ ↔ ψ))
6	5	notbid 285	. . . 4 ⊢ (x = y → (¬ φ ↔ ¬ ψ))
7	2, 4, 6	cbval 1984	. . 3 ⊢ (∀x ¬ φ ↔ ∀y ¬ ψ)
8	7	notbii 287	. 2 ⊢ (¬ ∀x ¬ φ ↔ ¬ ∀y ¬ ψ)
9		df-ex 1542	. 2 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
10		df-ex 1542	. 2 ⊢ (∃yψ ↔ ¬ ∀y ¬ ψ)
11	8, 9, 10	3bitr4i 268	1 ⊢ (∃xφ ↔ ∃yψ)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176  ∀wal 1540  ∃wex 1541  Ⅎwnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  cbvexv  2003  cbvex2  2005  exsb  2130  euf  2210  mo  2226  cbvmo  2241  mopick  2266  clelab  2473  issetf  2864  eqvincf  2967  rexab2  3003  euabsn  3792  eluniab  3903  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  opeliunxp  4820  dfdmf  4905  dfrnf  4962  cbvoprab1  5567  cbvoprab2  5568