Metamath Proof Explorer


Theorem iinssiin

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses iinssiin.1 x φ
iinssiin.2 φ x A B C
Assertion iinssiin φ x A B x A C

Proof

Step Hyp Ref Expression
1 iinssiin.1 x φ
2 iinssiin.2 φ x A B C
3 nfii1 _ x x A B
4 3 nfcri x y x A B
5 1 4 nfan x φ y x A B
6 2 adantlr φ y x A B x A B C
7 eliinid y x A B x A y B
8 7 adantll φ y x A B x A y B
9 6 8 sseldd φ y x A B x A y C
10 9 ex φ y x A B x A y C
11 5 10 ralrimi φ y x A B x A y C
12 eliin y V y x A C x A y C
13 12 elv y x A C x A y C
14 11 13 sylibr φ y x A B y x A C
15 14 ssd φ x A B x A C