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	⊢ 𝐴 ∈ V
	intpr.2	⊢ 𝐵 ∈ V
Assertion	intpr	⊢ ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		intpr.1	⊢ 𝐴 ∈ V
2		intpr.2	⊢ 𝐵 ∈ V
3		19.26	⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
4		vex	⊢ 𝑦 ∈ V
5	4	elpr	⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
6	5	imbi1i	⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 ) )
7		jaob	⊢ ( ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
8	6 7	bitri	⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
9	8	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
10	1	clel4	⊢ ( 𝑥 ∈ 𝐴 ↔ ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) )
11	2	clel4	⊢ ( 𝑥 ∈ 𝐵 ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) )
12	10 11	anbi12i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
13	3 9 12	3bitr4i	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
14		vex	⊢ 𝑥 ∈ V
15	14	elint	⊢ ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) )
16		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
17	13 15 16	3bitr4i	⊢ ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
18	17	eqriv	⊢ ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 )