Metamath Proof Explorer

Theorem fvimacnvi

Description: A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007)

Ref Expression
Assertion fvimacnvi ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F ⁡ A ∈ B

Proof

Step Hyp Ref Expression
1 snssi ⊢ A ∈ F -1 B → A ⊆ F -1 B
2 funimass2 ⊢ Fun ⁡ F ∧ A ⊆ F -1 B → F A ⊆ B
3 1 2 sylan2 ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F A ⊆ B
4 fvex ⊢ F ⁡ A ∈ V
5 4 snss ⊢ F ⁡ A ∈ B ↔ F ⁡ A ⊆ B
6 cnvimass ⊢ F -1 B ⊆ dom ⁡ F
7 6 sseli ⊢ A ∈ F -1 B → A ∈ dom ⁡ F
8 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
9 fnsnfv ⊢ F Fn dom ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = F A
10 8 9 sylanb ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = F A
11 7 10 sylan2 ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F ⁡ A = F A
12 11 sseq1d ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F ⁡ A ⊆ B ↔ F A ⊆ B
13 5 12 syl5bb ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F ⁡ A ∈ B ↔ F A ⊆ B
14 3 13 mpbird ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F ⁡ A ∈ B