Definition df-3o 8516

Description: Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-3o	⊢ 3o = suc 2o

Detailed syntax breakdown of Definition df-3o

Step	Hyp	Ref	Expression
1		c3o 8509	. 2 class 3o
2		c2o 8508	. . 3 class 2o
3	2	csuc 6390	. 2 class suc 2o
4	1, 3	wceq 1570	1 wff 3o = suc 2o

This definition is used by:  ord3  8530  3on  8531  o2p2e4  8587  3onn  8691  en3  9310  hash3  14591  2olt9o  35920  gdlopcfv3  36015  gdlopcfv4  36016  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  gdlopcfv8  36020  finxp3o  38591  df3o2  44576  df3o3  44577  omcl3g  44597  nlim3  44706  tr3dom  44790  har2o  44808  clsk1independent  45307  par2catid  51098  parswapprop  51108