Theorem iinss2 4502

Description: An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.)

Assertion

Ref	Expression
iinss2	⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵)

Proof of Theorem iinss2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3175	. . . 4 ⊢ 𝑦 ∈ V
2		eliin 4455	. . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3	1, 2	ax-mp 5	. . 3 ⊢ (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4		rsp 2912	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵))
5	4	com12 32	. . 3 ⊢ (𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵))
6	3, 5	syl5bi 230	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐵))
7	6	ssrdv 3573	1 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 194   ∈ wcel 1976  ∀wral 2895  Vcvv 3172   ⊆ wss 3539  ∩ ciin 4450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174  df-in 3546  df-ss 3553  df-iin 4452

This theorem is referenced by:  dmiin  5277  gruiin  9488  txtube  21195  iooiinicc  38420  iooiinioc  38434  meaiininclem  39180