Definition df-ltc 6101

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 6091	. 2 class <c
2		clec 6090	. . 3 class ≤c
3		cid 4764	. . 3 class I
4	2, 3	cdif 3207	. 2 class ( ≤c ∖ I )
5	1, 4	wceq 1642	1 wff <c = ( ≤c ∖ I )

This definition is referenced by:  brltc  6115  ltcex  6117