Definition df-in 2022

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 2215 and dfin4 2219. For intersection defined in terms of union, see dfin3 2218.

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cin 2017	. 2 class (A i^i B)
4		vx	. . . . . 6 set x
5	4	cv 1098	. . . . 5 class x
6	5, 1	wcel 1105	. . . 4 wff x e. A
7	5, 2	wcel 1105	. . . 4 wff x e. B
8	6, 7	wa 223	. . 3 wff (x e. A /\ x e. B)
9	8, 4	cab 1440	. 2 class {x | (x e. A /\ x e. B)}
10	3, 9	wceq 1099	1 wff (A i^i B) = {x | (x e. A /\ x e. B)}

This definition is referenced by:  dfin5 2023  dfss2 2029  elin 2178  disj 2282

Copyright terms: Public domain