Metamath Proof Explorer - mmascii

Symbol to ASCII Correspondence for Text-Only Browsers (in order of first appearance)

Symbol	ASCII
(	(
)	)
→	->
¬	-.
wff	wff
⊢	|-
φ	ph
ψ	ps
χ	ch
θ	th
τ	ta
↔	<->
∨	\/
∧	/\
η	et
ζ	ze
∀	A.
set	set
x	x
y	y
z	z
w	w
v	v
∃	E.
=	=
∈	e.
[	[
/	/
]	]
u	u
f	f
g	g
∃!	E!
∃*	E*
t	t
{	{
∣	|
}	}
class	class
A	A
B	B
C	C
D	D
R	R
S	S
T	T
F	F
G	G
≠	=/=
∉	e/
V	V
∖	\
∪	u.
∩	i^i
⊆	(_
⊂	(.
∅	(/)
if	if
,	,
σ	si
ρ	rh
℘	P~
⟨	<.
⟩	>.
∪	U.
∩	|^|
Tr	Tr
E	E
I	I
Po	Po
Or	Or
sup	sup
Fr	Fr
We	We
Ord	Ord
On	On
Lim	Lim
suc	suc
ω	om
×	X.
◡	`'
dom	dom
ran	ran
↾	|`
“	"
∘	o.
Rel	Rel
Fun	Fun
Fn	Fn
:	:
–→	-->
–1-1→	-1-1->
–onto→	-onto->
–1-1-onto→	-1-1-onto->
‘	`
Isom	Isom
h	h
H	H
rec	rec
1st	1st
2nd	2nd
1o	1o
2o	2o
+o	+o
·o	.o
↑o	^o
Er	Er
/	/.
Q	Q
s	s
r	r
a	a
b	b
c	c
d	d
J	J
K	K
L	L
M	M
N	N
W	W
X	X
Y	Y
Z	Z
↑m	^m
≈	~~
≼	~<_
≺	~<
R1	R1
rank	rank
q	q
j	j
k	k
m	m
n	n
card	card
ℵ	aleph
cf	cf
Card	Card
+c	+c
N	N.
+N	+N
·N	.N
<N	<N
+pQ	+pQ
·pQ	.pQ
~Q	~Q
Q	Q.
1Q	1Q
+Q	+Q
·Q	.Q
*Q	*Q
<Q	<Q
P	P.
1P	1P
+P	+P.
·P	.P
<P	<P
+pR	+pR
·pR	.pR
~R	~R
R	R.
0R	0R
1R	1R
-1R	-1R
+R	+R
·R	.R
<R	<R
ℂ	CC
ℝ	RR
0	0
1	1
i	i
+	+
·	x.
<	<
−	-
-	-u
≤	<_
ℕ	NN
ℕ0	NN0
ℤ	ZZ
ℚ	QQ
2	2
3	3
4	4
5	5
6	6
7	7
8	8
9	9
floor	floor
seq	seq
↑	^
√	sqr
ℜ	Re
ℑ	Im
∗	*
abs	abs
!	!
⇝	~~>
ℋ	H~
+v	+v
·s	.s
0v	0v
−v	-v
·i	.i
norm	norm
Cauchy	Cauchy
⇝v	~~>v
Sℋ	SH
Cℋ	CH
⊥	_|_
+ℋ	+H
span	span
∨ℋ	vH
∨ℋ	\/H
0ℋ	0H
Com	Com
Proj	Proj
+P	+P
−P	-P
States	States
Atoms	Atoms
Mℋ	MH
⋖	<o
p	p

metamath.org