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 |
⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶 ) |