Theorem cbvex 849

Description: Rule used to change bound variables with implicit substitution.

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	hbne 699	. . . 4 ⊢ (¬ φ → ∀y ¬ φ)
3		cbvex.2	. . . . 5 ⊢ (ψ → ∀xψ)
4	3	hbne 699	. . . 4 ⊢ (¬ ψ → ∀x ¬ ψ)
5		cbvex.3	. . . . 5 ⊢ (x = y → (φ ↔ ψ))
6	5	negbid 463	. . . 4 ⊢ (x = y → (¬ φ ↔ ¬ ψ))
7	2, 4, 6	cbval 848	. . 3 ⊢ (∀x ¬ φ ↔ ∀y ¬ ψ)
8	7	negbii 162	. 2 ⊢ (¬ ∀x ¬ φ ↔ ¬ ∀y ¬ ψ)
9		df-ex 679	. 2 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
10		df-ex 679	. 2 ⊢ (∃yψ ↔ ¬ ∀y ¬ ψ)
11	8, 9, 10	3bitr4 158	1 ⊢ (∃xφ ↔ ∃yψ)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127  ∀wal 672  ∃wex 678   = weq 797

This theorem is referenced by:  cbvexv 973  cbvex2 975  euf 1011  mo 1020  cbvmo 1034  mopick 1054  clelab 1187  cbvrex 1332  vtoclgf 1382  cla4gf 1394  eqvincf 1408  axrep 1473  zfrep2 1475  abn0 1715  eusn 1913  eluniab 1926  opabid 2099  cbvopab1 2106  cbvopab1s 2107  dfdmf 2526  dfrnf 2561  zfcndrep 3760  nnwof 4609

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org