Theorem riinn0 5045

Description: Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)

Assertion

Ref	Expression
riinn0	⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑋

Allowed substitution hint:   𝑆(𝑥)

Proof of Theorem riinn0

Step	Hyp	Ref	Expression
1		incom 4108	. 2 ⊢ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = (∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴)
2		r19.2z 4457	. . . . 5 ⊢ ((𝑋 ≠ ∅ ∧ ∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴) → ∃𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴)
3	2	ancoms 464	. . . 4 ⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → ∃𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴)
4		iinss 5017	. . . 4 ⊢ (∃𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 → ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴)
5	3, 4	syl 18	. . 3 ⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → ∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴)
6		dfss2 4096	. . 3 ⊢ (∩ 𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ↔ (∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴) = ∩ 𝑥 ∈ 𝑋 𝑆)
7	5, 6	sylib 221	. 2 ⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (∩ 𝑥 ∈ 𝑋 𝑆 ∩ 𝐴) = ∩ 𝑥 ∈ 𝑋 𝑆)
8	1, 7	eqtrid 2810	1 ⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ≠ wne 2958  ∀wral 3079  ∃wrex 3089   ⊆ wss 3899   ∩ cin 4091  ∅c0 4280  ∩ ciin 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-nul 4281  df-iin 4956

This theorem is used by:  riinrab  5046  riiner  8822  mreriincl  17780  riinopn  23238  alexsublem  24375  fnemeet1  37281