Metamath Proof Explorer

Theorem eliin2f

Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis eliin2f.1 ⊢ Ⅎ _ x B
Assertion eliin2f ⊢ B ≠ ∅ → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C

Proof

Step Hyp Ref Expression
1 eliin2f.1 ⊢ Ⅎ _ x B
2 eliin ⊢ A ∈ V → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C
3 2 adantl ⊢ B ≠ ∅ ∧ A ∈ V → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C
4 prcnel ⊢ ¬ A ∈ V → ¬ A ∈ ⋂ x ∈ B C
5 4 adantl ⊢ B ≠ ∅ ∧ ¬ A ∈ V → ¬ A ∈ ⋂ x ∈ B C
6 n0 ⊢ B ≠ ∅ ↔ ∃ y y ∈ B
7 6 biimpi ⊢ B ≠ ∅ → ∃ y y ∈ B
8 7 adantr ⊢ B ≠ ∅ ∧ ¬ A ∈ V → ∃ y y ∈ B
9 prcnel ⊢ ¬ A ∈ V → ¬ A ∈ ⦋ y / x⦌ C
10 9 a1d ⊢ ¬ A ∈ V → y ∈ B → ¬ A ∈ ⦋ y / x⦌ C
11 10 adantl ⊢ B ≠ ∅ ∧ ¬ A ∈ V → y ∈ B → ¬ A ∈ ⦋ y / x⦌ C
12 11 ancld ⊢ B ≠ ∅ ∧ ¬ A ∈ V → y ∈ B → y ∈ B ∧ ¬ A ∈ ⦋ y / x⦌ C
13 12 eximdv ⊢ B ≠ ∅ ∧ ¬ A ∈ V → ∃ y y ∈ B → ∃ y y ∈ B ∧ ¬ A ∈ ⦋ y / x⦌ C
14 8 13 mpd ⊢ B ≠ ∅ ∧ ¬ A ∈ V → ∃ y y ∈ B ∧ ¬ A ∈ ⦋ y / x⦌ C
15 df-rex ⊢ ∃ y ∈ B ¬ A ∈ ⦋ y / x⦌ C ↔ ∃ y y ∈ B ∧ ¬ A ∈ ⦋ y / x⦌ C
16 14 15 sylibr ⊢ B ≠ ∅ ∧ ¬ A ∈ V → ∃ y ∈ B ¬ A ∈ ⦋ y / x⦌ C
17 nfcv ⊢ Ⅎ _ y B
18 nfv ⊢ Ⅎ y ¬ A ∈ C
19 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ C
20 19 nfel2 ⊢ Ⅎ x A ∈ ⦋ y / x⦌ C
21 20 nfn ⊢ Ⅎ x ¬ A ∈ ⦋ y / x⦌ C
22 csbeq1a ⊢ x = y → C = ⦋ y / x⦌ C
23 22 eleq2d ⊢ x = y → A ∈ C ↔ A ∈ ⦋ y / x⦌ C
24 23 notbid ⊢ x = y → ¬ A ∈ C ↔ ¬ A ∈ ⦋ y / x⦌ C
25 1 17 18 21 24 cbvrexfw ⊢ ∃ x ∈ B ¬ A ∈ C ↔ ∃ y ∈ B ¬ A ∈ ⦋ y / x⦌ C
26 16 25 sylibr ⊢ B ≠ ∅ ∧ ¬ A ∈ V → ∃ x ∈ B ¬ A ∈ C
27 rexnal ⊢ ∃ x ∈ B ¬ A ∈ C ↔ ¬ ∀ x ∈ B A ∈ C
28 26 27 sylib ⊢ B ≠ ∅ ∧ ¬ A ∈ V → ¬ ∀ x ∈ B A ∈ C
29 5 28 2falsed ⊢ B ≠ ∅ ∧ ¬ A ∈ V → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C
30 3 29 pm2.61dan ⊢ B ≠ ∅ → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C