Metamath Proof Explorer

Theorem ssiin

Description: Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003)

Ref Expression
Assertion ssiin 
|- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ x C
2 1 ssiinf 
 |-  ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )