ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-se GIF version

Definition df-se 4056
Description: Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
Assertion
Ref Expression
df-se (𝑅 Se Ax A {y Ay𝑅x} V)
Distinct variable groups:   x,y,𝑅   x,A,y

Detailed syntax breakdown of Definition df-se
StepHypRef Expression
1 cA . . 3 class A
2 cR . . 3 class 𝑅
31, 2wse 4055 . 2 wff 𝑅 Se A
4 vy . . . . . . 7 setvar y
54cv 1241 . . . . . 6 class y
6 vx . . . . . . 7 setvar x
76cv 1241 . . . . . 6 class x
85, 7, 2wbr 3755 . . . . 5 wff y𝑅x
98, 4, 1crab 2304 . . . 4 class {y Ay𝑅x}
10 cvv 2551 . . . 4 class V
119, 10wcel 1390 . . 3 wff {y Ay𝑅x} V
1211, 6, 1wral 2300 . 2 wff x A {y Ay𝑅x} V
133, 12wb 98 1 wff (𝑅 Se Ax A {y Ay𝑅x} V)
Colors of variables: wff set class
This definition is referenced by:  seex  4057  exse  4058  sess1  4059  sess2  4060  nfse  4063  epse  4064  seinxp  4354  dfse2  4641  exse2  4642
  Copyright terms: Public domain W3C validator