Definition df-ltc 6100

Description: Define cardinal less than. Definition from [Rosser] p. 375. (Contributed by Scott Fenton, 24-Feb-2015.)

Assertion

Ref	Expression
df-ltc	⊢ <c = ( ≤c ∖ I )

Detailed syntax breakdown of Definition df-ltc

Step	Hyp	Ref	Expression
1		cltc 6090	. 2 class <c
2		clec 6089	. . 3 class ≤c
3		cid 4763	. . 3 class I
4	2, 3	cdif 3206	. 2 class ( ≤c ∖ I )
5	1, 4	wceq 1642	1 wff <c = ( ≤c ∖ I )

This definition is referenced by:  brltc  6114  ltcex  6116