Theorem cbvexv 973

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

Hypothesis

Ref	Expression
cbvalv.1	⊢ (x = y → (φ ↔ ψ))

Assertion

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

Distinct variable group(s):   φ,y   ψ,x

Proof of Theorem cbvexv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (φ → ∀yφ)
2		ax-17 925	. 2 ⊢ (ψ → ∀xψ)
3		cbvalv.1	. 2 ⊢ (x = y → (φ ↔ ψ))
4	1, 2, 3	cbvex 849	1 ⊢ (∃xφ ↔ ∃yψ)

Syntax hints:   → wi 2   ↔ wb 127  ∃wex 678   = weq 797

This theorem is referenced by:  axun 1081  axac 1085  bm1.3ii 1481  cbvopab1v 2108  cbvopab2v 2109  fv3 2839  rdglem2 2976  aceq1 3552  aceq0 3553  aceq3lem 3555  aceq4 3557  kmlem2 3581  kmlem12 3591  zfcndun 3761  zfcndac 3765  sup2 4510  infxpidmlem2 4934

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  ax-17 925

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

metamath.org