Metamath Proof Explorer

Theorem fimarab

Description: Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Assertion fimarab ⊢ F : A ⟶ B ∧ X ⊆ A → F X = y ∈ B | ∃ x ∈ X F ⁡ x = y

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ y F : A ⟶ B ∧ X ⊆ A
2 nfcv ⊢ Ⅎ _ y F X
3 nfrab1 ⊢ Ⅎ _ y y ∈ B | ∃ x ∈ X F ⁡ x = y
4 ffn ⊢ F : A ⟶ B → F Fn A
5 fvelimab ⊢ F Fn A ∧ X ⊆ A → y ∈ F X ↔ ∃ x ∈ X F ⁡ x = y
6 5 anbi2d ⊢ F Fn A ∧ X ⊆ A → y ∈ B ∧ y ∈ F X ↔ y ∈ B ∧ ∃ x ∈ X F ⁡ x = y
7 4 6 sylan ⊢ F : A ⟶ B ∧ X ⊆ A → y ∈ B ∧ y ∈ F X ↔ y ∈ B ∧ ∃ x ∈ X F ⁡ x = y
8 fimass ⊢ F : A ⟶ B → F X ⊆ B
9 8 adantr ⊢ F : A ⟶ B ∧ X ⊆ A → F X ⊆ B
10 9 sseld ⊢ F : A ⟶ B ∧ X ⊆ A → y ∈ F X → y ∈ B
11 10 pm4.71rd ⊢ F : A ⟶ B ∧ X ⊆ A → y ∈ F X ↔ y ∈ B ∧ y ∈ F X
12 rabid ⊢ y ∈ y ∈ B | ∃ x ∈ X F ⁡ x = y ↔ y ∈ B ∧ ∃ x ∈ X F ⁡ x = y
13 12 a1i ⊢ F : A ⟶ B ∧ X ⊆ A → y ∈ y ∈ B | ∃ x ∈ X F ⁡ x = y ↔ y ∈ B ∧ ∃ x ∈ X F ⁡ x = y
14 7 11 13 3bitr4d ⊢ F : A ⟶ B ∧ X ⊆ A → y ∈ F X ↔ y ∈ y ∈ B | ∃ x ∈ X F ⁡ x = y
15 1 2 3 14 eqrd ⊢ F : A ⟶ B ∧ X ⊆ A → F X = y ∈ B | ∃ x ∈ X F ⁡ x = y