Theorem iinssiin 45645

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
iinssiin.1	⊢ Ⅎ𝑥𝜑
iinssiin.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
iinssiin	⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶)

Proof of Theorem iinssiin

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iinssiin.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
2		nfii1 4976	. . . . . 6 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵
3	2	nfcri 2906	. . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵
4	1, 3	nfan 1909	. . . 4 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵)
5		iinssiin.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
6	5	adantlr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
7		eliinid 45627	. . . . . . 7 ⊢ ((𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)
8	7	adantll 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)
9	6, 8	sseldd 3928	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐶)
10	9	ex 415	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐶))
11	4, 10	ralrimi 3250	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) → ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
12		eliin 4944	. . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
13	12	elv 3449	. . 3 ⊢ (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
14	11, 13	sylibr 236	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) → 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶)
15	14	ssd 45598	1 ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  Ⅎwnf 1793   ∈ wcel 2132  ∀wral 3066  Vcvv 3444   ⊆ wss 3895  ∩ ciin 4940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1553  df-ex 1790  df-nf 1794  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ral 3067  df-v 3446  df-ss 3912  df-iin 4942

This theorem is referenced by: (None)