Theorem inixp

Description: Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	inixp	⊢ ( X 𝑥 ∈ 𝐴 𝐵 ∩ X 𝑥 ∈ 𝐴 𝐶 ) = X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		an4	⊢ ( ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( ( 𝑓 Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
2		anidm	⊢ ( ( 𝑓 Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) ↔ 𝑓 Fn 𝐴 )
3		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
4		elin	⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
5	4	bicomi	⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) )
6	5	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) )
7	3 6	bitr3i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) )
8	2 7	anbi12i	⊢ ( ( ( 𝑓 Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) )
9	1 8	bitri	⊢ ( ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) )
10		vex	⊢ 𝑓 ∈ V
11	10	elixp	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
12	10	elixp	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
13	11 12	anbi12i	⊢ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) ↔ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) )
14	10	elixp	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝐵 ∩ 𝐶 ) ) )
15	9 13 14	3bitr4i	⊢ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐶 ) ↔ 𝑓 ∈ X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) )
16	15	ineqri	⊢ ( X 𝑥 ∈ 𝐴 𝐵 ∩ X 𝑥 ∈ 𝐴 𝐶 ) = X 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 )