= Solution
Choose distinct fresh parameters $a,b$. Within the assumption $a=b$, <equality elimination rule> gives the forward implication directly. Derive the reverse equality explicitly before using it for the reverse implication:
``
1 | a = b assumption
2 | | P(a) assumption
3 | | P(b) =-elim 1,2
4 | P(a) → P(b) →-intro 2–3
5 | a = a =-intro
6 | b = a =-elim 1,5; φ(u) := (u = a)
7 | | P(b) assumption
8 | | P(a) =-elim 6,7
9 | P(b) → P(a) →-intro 7–8
10 | (P(a) → P(b)) ∧ (P(b) → P(a)) ∧-intro 4,9
11 a = b → ((P(a) → P(b)) ∧ (P(b) → P(a))) →-intro 1–10
12 ∀y. a = y → ((P(a) → P(y)) ∧ (P(y) → P(a))) ∀-intro 11, b fresh
13 ∀x. ∀y. x = y → ((P(x) → P(y)) ∧ (P(y) → P(x))) ∀-intro 12, a fresh
``
The equality assumption is discharged before either <universal quantifier introduction rule>. There are then no undischarged assumptions, so both <eigenvariable condition> requirements hold. The final \b[universal theorem] expresses that equal arguments are interchangeable in the <predicate> $P$ in both directions.
Back to article page
