Theorem iinss 5014

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 4955	. . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
2	1	elv 3455	. . 3 ⊢ (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3		ssel 3902	. . . . 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 3914	1 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

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

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 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3896  df-iin 4953

This theorem is used by:  riinn0  5042  reliin  5794  cnviin  6289  iiner  8814  scott0b  9941  scott0OLD  9942  cfslb  10348  ptbasfi  23906  iscmet3  25620  fnemeet1  37247  pmapglb2N  40922  pmapglb2xN  40923  iinssd  46240  iooiinicc  46648  iooiinioc  46662  meaiininclem  47590  iinhoiicclem  47777  smflim  47881  smflimsuplem7  47930  iinglb  50027  iineqconst2  50029  iinfssc  50265