Metamath Proof Explorer

Theorem iinexg

Description: The existence of a class intersection. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by FL, 19-Sep-2011)

Ref Expression
Assertion iinexg ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B ∈ V

Proof

Step Hyp Ref Expression
1 dfiin2g ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B
2 1 adantl ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B
3 elisset ⊢ B ∈ C → ∃ y y = B
4 3 rgenw ⊢ ∀ x ∈ A B ∈ C → ∃ y y = B
5 r19.2z ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → ∃ y y = B → ∃ x ∈ A B ∈ C → ∃ y y = B
6 4 5 mpan2 ⊢ A ≠ ∅ → ∃ x ∈ A B ∈ C → ∃ y y = B
7 r19.35 ⊢ ∃ x ∈ A B ∈ C → ∃ y y = B ↔ ∀ x ∈ A B ∈ C → ∃ x ∈ A ∃ y y = B
8 6 7 sylib ⊢ A ≠ ∅ → ∀ x ∈ A B ∈ C → ∃ x ∈ A ∃ y y = B
9 8 imp ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → ∃ x ∈ A ∃ y y = B
10 rexcom4 ⊢ ∃ x ∈ A ∃ y y = B ↔ ∃ y ∃ x ∈ A y = B
11 9 10 sylib ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → ∃ y ∃ x ∈ A y = B
12 abn0 ⊢ y | ∃ x ∈ A y = B ≠ ∅ ↔ ∃ y ∃ x ∈ A y = B
13 11 12 sylibr ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → y | ∃ x ∈ A y = B ≠ ∅
14 intex ⊢ y | ∃ x ∈ A y = B ≠ ∅ ↔ ⋂ y | ∃ x ∈ A y = B ∈ V
15 13 14 sylib ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → ⋂ y | ∃ x ∈ A y = B ∈ V
16 2 15 eqeltrd ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B ∈ V