Theorem cbval 1163

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

Hypotheses

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

Assertion

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

Proof of Theorem cbval

Step	Hyp	Ref	Expression
1		cbval.1	. . . 4 ⊢ (φ → ∀yφ)
2	1	imim2i 17	. . 3 ⊢ ((φ → φ) → (φ → ∀yφ))
3		cbval.2	. . . 4 ⊢ (ψ → ∀xψ)
4	3	a1i 8	. . 3 ⊢ ((φ → φ) → (ψ → ∀xψ))
5		cbval.3	. . . 4 ⊢ (x = y → (φ ↔ ψ))
6	5	a1i 8	. . 3 ⊢ ((φ → φ) → (x = y → (φ ↔ ψ)))
7	2, 4, 6	cbv2 1161	. 2 ⊢ (∀x∀y(φ → φ) → (∀xφ ↔ ∀yψ))
8		id 59	. . 3 ⊢ (φ → φ)
9	8	ax-gen 961	. 2 ⊢ ∀y(φ → φ)
10	7, 9	mpg 984	1 ⊢ (∀xφ ↔ ∀yψ)

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 952   = wceq 954

This theorem is referenced by:  cbvex 1164  cbvalv 1312  cbval2 1314  cbvald 1318  cleqf 1557  cbvralf 1793  dfss2f 2056  elintab 2539  ssintab 2545  dffunmof 3522  aceq1 4709  nnwof 6399  homcard 10462

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

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

Copyright terms: Public domain