Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter II with equivalence of sets
frege54cor1b
Next ⟩
frege55lem1b
Metamath Proof Explorer
Ascii
Structured
Theorem
frege54cor1b
Description:
Reflexive equality.
(Contributed by
RP
, 24-Dec-2019)
Ref
Expression
Assertion
frege54cor1b
⊢
[
𝑥
/
𝑦
]
𝑦
=
𝑥
Proof
Step
Hyp
Ref
Expression
1
equsb1
⊢
[
𝑥
/
𝑦
]
𝑦
=
𝑥