HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-in 2866
Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3072 and dfin4 3076. For intersection defined in terms of union, see dfin3 3075.
Assertion
Ref Expression
df-in |- (A i^i B) = {x | (x e. A /\ x e. B)}
Distinct variable groups:   x,A   x,B

Detailed syntax breakdown of Definition df-in
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cin 2858 . 2 class (A i^i B)
4 vx . . . . . 6 set x
54cv 1614 . . . . 5 class x
65, 1wcel 1617 . . . 4 wff x e. A
75, 2wcel 1617 . . . 4 wff x e. B
86, 7wa 433 . . 3 wff (x e. A /\ x e. B)
98, 4cab 2157 . 2 class {x | (x e. A /\ x e. B)}
103, 9wceq 1615 1 wff (A i^i B) = {x | (x e. A /\ x e. B)}
Colors of variables: wff set class
This definition is referenced by:  dfin5 2867  dfss2 2873  elin 3031  disj 3150  csbingVD 17803
Copyright terms: Public domain