HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-int 2524
Description: Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44.
Assertion
Ref Expression
df-int |- |^|A = {x | A.y(y e. A -> x e. y)}
Distinct variable group:   x,y,A
Detailed syntax breakdown of Definition df-int
StepHypRef Expression
1 cA . . 3 class A
21cint 2523 . 2 class |^|A
3 vy . . . . . . 7 set y
43cv 952 . . . . . 6 class y
54, 1wcel 955 . . . . 5 wff y e. A
6 vx . . . . . . 7 set x
76cv 952 . . . . . 6 class x
87, 4wcel 955 . . . . 5 wff x e. y
95, 8wi 3 . . . 4 wff (y e. A -> x e. y)
109, 3wal 951 . . 3 wff A.y(y e. A -> x e. y)
1110, 6cab 1456 . 2 class {x | A.y(y e. A -> x e. y)}
122, 11wceq 953 1 wff |^|A = {x | A.y(y e. A -> x e. y)}
Colors of variables: wff set class
This definition is referenced by:  dfint2 2525  elint 2529  int0 2537  dfiin2 2578
Copyright terms: Public domain