Theorem cbvalv 1318

Description: Rule used to change bound variables, using implicit substitition.

Hypothesis

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

Assertion

Ref	Expression
cbvalv	⊢ (∀xφ ↔ ∀yψ)

Distinct variable groups:   φ,y   ψ,x

Proof of Theorem cbvalv

Step	Hyp	Ref	Expression
1		ax-17 975	. 2 ⊢ (φ → ∀yφ)
2		ax-17 975	. 2 ⊢ (ψ → ∀xψ)
3		cbvalv.1	. 2 ⊢ (x = y → (φ ↔ ψ))
4	1, 2, 3	cbval 1169	1 ⊢ (∀xφ ↔ ∀yψ)

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 958   = wceq 960

This theorem is referenced by:  axpow 2759  pssnn 4554  unifi 4573  fodomfi 4581  axinf 4640  aceq0 4747  aceq3 4750  aceq5 4757  axac 4762  kmlem1 4782  kmlem13 4794  zfcndpow 4988  zfcndinf 4990  zfcndac 4991  axgroth4 8804

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain