Theorem iinss 5015

Description: Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
iinss	⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem iinss

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eliin 4956	. . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
2	1	elv 3455	. . 3 ⊢ (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3		ssel 3925	. . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	reximi 3100	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		r19.36v 3190	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	4, 5	syl 18	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7	2, 6	biimtrid 245	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
8	7	ssrdv 3937	1 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3899  ∩ ciin 4952

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3916  df-iin 4954

This theorem is used by:  riinn0  5043  reliin  5798  cnviin  6284  iiner  8789  scott0b  9876  scott0OLD  9877  cfslb  10268  ptbasfi  23807  iscmet3  25521  fnemeet1  36985  pmapglb2N  40644  pmapglb2xN  40645  iinssd  45963  iooiinicc  46372  iooiinioc  46386  meaiininclem  47314  iinhoiicclem  47501  smflim  47605  smflimsuplem7  47654  iinglb  49750  iineqconst2  49752  iinfssc  49983