Theorem iinss 4571

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	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )

Distinct variable group:   x, C

Allowed substitution hints:   A( x)   B( x)

Proof of Theorem iinss

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3203	. . . 4 |- y e. _V
2		eliin 4525	. . . 4 |- ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
3	1, 2	ax-mp 5	. . 3 |- ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
4		ssel 3597	. . . . 5 |- ( B C_ C -> ( y e. B -> y e. C ) )
5	4	reximi 3011	. . . 4 |- ( E. x e. A B C_ C -> E. x e. A ( y e. B -> y e. C ) )
6		r19.36v 3085	. . . 4 |- ( E. x e. A ( y e. B -> y e. C ) -> ( A. x e. A y e. B -> y e. C ) )
7	5, 6	syl 17	. . 3 |- ( E. x e. A B C_ C -> ( A. x e. A y e. B -> y e. C ) )
8	3, 7	syl5bi 232	. 2 |- ( E. x e. A B C_ C -> ( y e. |^|_ x e. A B -> y e. C ) )
9	8	ssrdv 3609	1 |- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )

Syntax hints:   -> wi 4   <-> wb 196   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   C_ wss 3574   |^|_ciin 4521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-iin 4523

This theorem is referenced by:  riinn0  4595  reliin  5240  cnviin  5672  iiner  7819  scott0  8749  cfslb  9088  ptbasfi  21384  iscmet3  23091  fnemeet1  32361  pmapglb2N  35057  pmapglb2xN  35058  iinssd  39314  iooiinicc  39769  iooiinioc  39783  meaiininclem  40700  iinhoiicclem  40887  smflim  40985  smflimsuplem7  41032