Metamath Proof Explorer


Theorem iinssiin

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

Ref Expression
Hypotheses iinssiin.1 𝑥 𝜑
iinssiin.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝐶 )
Assertion iinssiin ( 𝜑 𝑥𝐴 𝐵 𝑥𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 iinssiin.1 𝑥 𝜑
2 iinssiin.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝐶 )
3 nfii1 𝑥 𝑥𝐴 𝐵
4 3 nfcri 𝑥 𝑦 𝑥𝐴 𝐵
5 1 4 nfan 𝑥 ( 𝜑𝑦 𝑥𝐴 𝐵 )
6 2 adantlr ( ( ( 𝜑𝑦 𝑥𝐴 𝐵 ) ∧ 𝑥𝐴 ) → 𝐵𝐶 )
7 eliinid ( ( 𝑦 𝑥𝐴 𝐵𝑥𝐴 ) → 𝑦𝐵 )
8 7 adantll ( ( ( 𝜑𝑦 𝑥𝐴 𝐵 ) ∧ 𝑥𝐴 ) → 𝑦𝐵 )
9 6 8 sseldd ( ( ( 𝜑𝑦 𝑥𝐴 𝐵 ) ∧ 𝑥𝐴 ) → 𝑦𝐶 )
10 9 ex ( ( 𝜑𝑦 𝑥𝐴 𝐵 ) → ( 𝑥𝐴𝑦𝐶 ) )
11 5 10 ralrimi ( ( 𝜑𝑦 𝑥𝐴 𝐵 ) → ∀ 𝑥𝐴 𝑦𝐶 )
12 eliin ( 𝑦 ∈ V → ( 𝑦 𝑥𝐴 𝐶 ↔ ∀ 𝑥𝐴 𝑦𝐶 ) )
13 12 elv ( 𝑦 𝑥𝐴 𝐶 ↔ ∀ 𝑥𝐴 𝑦𝐶 )
14 11 13 sylibr ( ( 𝜑𝑦 𝑥𝐴 𝐵 ) → 𝑦 𝑥𝐴 𝐶 )
15 14 ssd ( 𝜑 𝑥𝐴 𝐵 𝑥𝐴 𝐶 )