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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 elint ⊢ ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) )
3 vex ⊢ 𝑦 ∈ V
4 3 elpr ⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
5 4 imbi1i ⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 ) )
6 jaob ⊢ ( ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
7 5 6 bitri ⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
8 7 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
9 19.26 ⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
10 2 8 9 3bitri ⊢ ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
11 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
12 clel4g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↔ ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ) )
13 clel4g ⊢ ( 𝐵 ∈ 𝑊 → ( 𝑥 ∈ 𝐵 ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
14 12 13 bi2anan9 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) ) )
15 11 14 bitr2id ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
16 10 15 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
17 16 alrimiv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∀ 𝑥 ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
18 dfcleq ⊢ ( ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
19 17 18 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )