This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )