Metamath Proof Explorer

Theorem elintfv

Description: Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021)

Ref Expression
Hypothesis elintfv.1 ⊢ X ∈ V
Assertion elintfv ⊢ F Fn A ∧ B ⊆ A → X ∈ ⋂ F B ↔ ∀ y ∈ B X ∈ F ⁡ y

Proof

Step Hyp Ref Expression
1 elintfv.1 ⊢ X ∈ V
2 1 elint ⊢ X ∈ ⋂ F B ↔ ∀ z z ∈ F B → X ∈ z
3 fvelimab ⊢ F Fn A ∧ B ⊆ A → z ∈ F B ↔ ∃ y ∈ B F ⁡ y = z
4 3 imbi1d ⊢ F Fn A ∧ B ⊆ A → z ∈ F B → X ∈ z ↔ ∃ y ∈ B F ⁡ y = z → X ∈ z
5 r19.23v ⊢ ∀ y ∈ B F ⁡ y = z → X ∈ z ↔ ∃ y ∈ B F ⁡ y = z → X ∈ z
6 4 5 bitr4di ⊢ F Fn A ∧ B ⊆ A → z ∈ F B → X ∈ z ↔ ∀ y ∈ B F ⁡ y = z → X ∈ z
7 6 albidv ⊢ F Fn A ∧ B ⊆ A → ∀ z z ∈ F B → X ∈ z ↔ ∀ z ∀ y ∈ B F ⁡ y = z → X ∈ z
8 ralcom4 ⊢ ∀ y ∈ B ∀ z F ⁡ y = z → X ∈ z ↔ ∀ z ∀ y ∈ B F ⁡ y = z → X ∈ z
9 eqcom ⊢ F ⁡ y = z ↔ z = F ⁡ y
10 9 imbi1i ⊢ F ⁡ y = z → X ∈ z ↔ z = F ⁡ y → X ∈ z
11 10 albii ⊢ ∀ z F ⁡ y = z → X ∈ z ↔ ∀ z z = F ⁡ y → X ∈ z
12 fvex ⊢ F ⁡ y ∈ V
13 eleq2 ⊢ z = F ⁡ y → X ∈ z ↔ X ∈ F ⁡ y
14 12 13 ceqsalv ⊢ ∀ z z = F ⁡ y → X ∈ z ↔ X ∈ F ⁡ y
15 11 14 bitri ⊢ ∀ z F ⁡ y = z → X ∈ z ↔ X ∈ F ⁡ y
16 15 ralbii ⊢ ∀ y ∈ B ∀ z F ⁡ y = z → X ∈ z ↔ ∀ y ∈ B X ∈ F ⁡ y
17 8 16 bitr3i ⊢ ∀ z ∀ y ∈ B F ⁡ y = z → X ∈ z ↔ ∀ y ∈ B X ∈ F ⁡ y
18 7 17 bitrdi ⊢ F Fn A ∧ B ⊆ A → ∀ z z ∈ F B → X ∈ z ↔ ∀ y ∈ B X ∈ F ⁡ y
19 2 18 bitrid ⊢ F Fn A ∧ B ⊆ A → X ∈ ⋂ F B ↔ ∀ y ∈ B X ∈ F ⁡ y