Definition df-int 2601

Description: Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44.

Assertion

Ref	Expression
df-int	⊢ ∩A = {x∣∀y(y ∈ A → x ∈ y)}

Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-int

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cint 2600	. 2 class ∩A
3		vy	. . . . . . 7 set y
4	3	cv 991	. . . . . 6 class y
5	4, 1	wcel 994	. . . . 5 wff y ∈ A
6		vx	. . . . . . 7 set x
7	6	cv 991	. . . . . 6 class x
8	7, 4	wcel 994	. . . . 5 wff x ∈ y
9	5, 8	wi 3	. . . 4 wff (y ∈ A → x ∈ y)
10	9, 3	wal 990	. . 3 wff ∀y(y ∈ A → x ∈ y)
11	10, 6	cab 1505	. 2 class {x∣∀y(y ∈ A → x ∈ y)}
12	2, 11	wceq 992	1 wff ∩A = {x∣∀y(y ∈ A → x ∈ y)}

This definition is referenced by:  dfint2 2602  elint 2606  int0 2614  dfiin2 2656  dfiin2g 11400

Copyright terms: Public domain