Definition df-in 2048

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 2241 and dfin4 2245. For intersection defined in terms of union, see dfin3 2244.

Assertion

Ref	Expression
df-in	⊢ (A ∩ B) = {x∣(x ∈ A ⋀ x ∈ 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 2043	. 2 class (A ∩ B)
4		vx	. . . . . 6 set x
5	4	cv 954	. . . . 5 class x
6	5, 1	wcel 957	. . . 4 wff x ∈ A
7	5, 2	wcel 957	. . . 4 wff x ∈ B
8	6, 7	wa 223	. . 3 wff (x ∈ A ⋀ x ∈ B)
9	8, 4	cab 1462	. 2 class {x∣(x ∈ A ⋀ x ∈ B)}
10	3, 9	wceq 955	1 wff (A ∩ B) = {x∣(x ∈ A ⋀ x ∈ B)}

This definition is referenced by:  dfin5 2049  dfss2 2055  elin 2204  disj 2308

Copyright terms: Public domain