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  2474  issetf  2865  eqvincf  2968  rexab2  3004  euabsn  3793  eluniab  3904  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  opeliunxp  4821  dfdmf  4906  dfrnf  4963  cbvoprab1  5568  cbvoprab2  5569