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