Theorem intprg

Description: The intersection of a pair is the intersection of its members. Closed form of intpr . Theorem 71 of Suppes p. 42. (Contributed by FL, 27-Apr-2008) (Proof shortened by BJ, 1-Sep-2024)

	Ref	Expression
Assertion	intprg	|- ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	elint	|- ( x e. |^| { A , B } <-> A. y ( y e. { A , B } -> x e. y ) )
3		vex	|- y e. _V
4	3	elpr	|- ( y e. { A , B } <-> ( y = A \/ y = B ) )
5	4	imbi1i	|- ( ( y e. { A , B } -> x e. y ) <-> ( ( y = A \/ y = B ) -> x e. y ) )
6		jaob	|- ( ( ( y = A \/ y = B ) -> x e. y ) <-> ( ( y = A -> x e. y ) /\ ( y = B -> x e. y ) ) )
7	5 6	bitri	|- ( ( y e. { A , B } -> x e. y ) <-> ( ( y = A -> x e. y ) /\ ( y = B -> x e. y ) ) )
8	7	albii	|- ( A. y ( y e. { A , B } -> x e. y ) <-> A. y ( ( y = A -> x e. y ) /\ ( y = B -> x e. y ) ) )
9		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 ) ) )
10	2 8 9	3bitri	|- ( x e. |^| { A , B } <-> ( A. y ( y = A -> x e. y ) /\ A. y ( y = B -> x e. y ) ) )
11		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
12		clel4g	|- ( A e. V -> ( x e. A <-> A. y ( y = A -> x e. y ) ) )
13		clel4g	|- ( B e. W -> ( x e. B <-> A. y ( y = B -> x e. y ) ) )
14	12 13	bi2anan9	|- ( ( A e. V /\ B e. W ) -> ( ( x e. A /\ x e. B ) <-> ( A. y ( y = A -> x e. y ) /\ A. y ( y = B -> x e. y ) ) ) )
15	11 14	bitr2id	|- ( ( A e. V /\ B e. W ) -> ( ( A. y ( y = A -> x e. y ) /\ A. y ( y = B -> x e. y ) ) <-> x e. ( A i^i B ) ) )
16	10 15	bitrid	|- ( ( A e. V /\ B e. W ) -> ( x e. |^| { A , B } <-> x e. ( A i^i B ) ) )
17	16	alrimiv	|- ( ( A e. V /\ B e. W ) -> A. x ( x e. |^| { A , B } <-> x e. ( A i^i B ) ) )
18		dfcleq	|- ( |^| { A , B } = ( A i^i B ) <-> A. x ( x e. |^| { A , B } <-> x e. ( A i^i B ) ) )
19	17 18	sylibr	|- ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) )