Theorem intpr

Description: The intersection of a pair is the intersection of its members. Theorem 71 of Suppes p. 42. (Contributed by NM, 14-Oct-1999)

	Ref	Expression
Hypotheses	intpr.1	|- A e. _V
	intpr.2	|- B e. _V
Assertion	intpr	|- |^| { A , B } = ( A i^i B )

Proof

Step	Hyp	Ref	Expression
1		intpr.1	|- A e. _V
2		intpr.2	|- B e. _V
3		19.26	|- ( A. y ( ( y = A -> x e. y ) /\ ( y = B -> x e. y ) ) <-> ( A. y ( y = A -> x e. y ) /\ A. y ( y = B -> x e. y ) ) )
4		vex	|- y e. _V
5	4	elpr	|- ( y e. { A , B } <-> ( y = A \/ y = B ) )
6	5	imbi1i	|- ( ( y e. { A , B } -> x e. y ) <-> ( ( y = A \/ y = B ) -> x e. y ) )
7		jaob	|- ( ( ( y = A \/ y = B ) -> x e. y ) <-> ( ( y = A -> x e. y ) /\ ( y = B -> x e. y ) ) )
8	6 7	bitri	|- ( ( y e. { A , B } -> x e. y ) <-> ( ( y = A -> x e. y ) /\ ( y = B -> x e. y ) ) )
9	8	albii	|- ( A. y ( y e. { A , B } -> x e. y ) <-> A. y ( ( y = A -> x e. y ) /\ ( y = B -> x e. y ) ) )
10	1	clel4	|- ( x e. A <-> A. y ( y = A -> x e. y ) )
11	2	clel4	|- ( x e. B <-> A. y ( y = B -> x e. y ) )
12	10 11	anbi12i	|- ( ( x e. A /\ x e. B ) <-> ( A. y ( y = A -> x e. y ) /\ A. y ( y = B -> x e. y ) ) )
13	3 9 12	3bitr4i	|- ( A. y ( y e. { A , B } -> x e. y ) <-> ( x e. A /\ x e. B ) )
14		vex	|- x e. _V
15	14	elint	|- ( x e. |^| { A , B } <-> A. y ( y e. { A , B } -> x e. y ) )
16		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
17	13 15 16	3bitr4i	|- ( x e. |^| { A , B } <-> x e. ( A i^i B ) )
18	17	eqriv	|- |^| { A , B } = ( A i^i B )