Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Andrew Salmon
Principia Mathematica * 13 and * 14
iotaequ
Next ⟩
iotavalb
Metamath Proof Explorer
Ascii
Unicode
Theorem
iotaequ
Description:
Theorem *14.2 in
WhiteheadRussell
p. 189.
(Contributed by
Andrew Salmon
, 11-Jul-2011)
Ref
Expression
Assertion
iotaequ
⊢
ι
x
|
x
=
y
=
y
Proof
Step
Hyp
Ref
Expression
1
iotaval
⊢
∀
x
x
=
y
↔
x
=
y
→
ι
x
|
x
=
y
=
y
2
biid
⊢
x
=
y
↔
x
=
y
3
1
2
mpg
⊢
ι
x
|
x
=
y
=
y