NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-lec GIF version

Definition df-lec 6099
Description: Define cardinal less than or equal. Definition from [Rosser] p. 375. (Contributed by Scott Fenton, 24-Feb-2015.)
Assertion
Ref Expression
df-lec c = {a, b x a y b x y}
Distinct variable group:   x,y,a,b

Detailed syntax breakdown of Definition df-lec
StepHypRef Expression
1 clec 6089 . 2 class c
2 vx . . . . . . 7 setvar x
32cv 1641 . . . . . 6 class x
4 vy . . . . . . 7 setvar y
54cv 1641 . . . . . 6 class y
63, 5wss 3257 . . . . 5 wff x y
7 vb . . . . . 6 setvar b
87cv 1641 . . . . 5 class b
96, 4, 8wrex 2615 . . . 4 wff y b x y
10 va . . . . 5 setvar a
1110cv 1641 . . . 4 class a
129, 2, 11wrex 2615 . . 3 wff x a y b x y
1312, 10, 7copab 4622 . 2 class {a, b x a y b x y}
141, 13wceq 1642 1 wff c = {a, b x a y b x y}
Colors of variables: wff setvar class
This definition is referenced by:  brlecg  6112
  Copyright terms: Public domain W3C validator