This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elmapsnd

Description: Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses elmapsnd.1 ⊢ φ → F Fn A
elmapsnd.2 ⊢ φ → B ∈ V
elmapsnd.3 ⊢ φ → F ⁡ A ∈ B
Assertion elmapsnd ⊢ φ → F ∈ B A

Proof

Step Hyp Ref Expression
1 elmapsnd.1 ⊢ φ → F Fn A
2 elmapsnd.2 ⊢ φ → B ∈ V
3 elmapsnd.3 ⊢ φ → F ⁡ A ∈ B
4 elsni ⊢ x ∈ A → x = A
5 4 fveq2d ⊢ x ∈ A → F ⁡ x = F ⁡ A
6 5 adantl ⊢ φ ∧ x ∈ A → F ⁡ x = F ⁡ A
7 3 adantr ⊢ φ ∧ x ∈ A → F ⁡ A ∈ B
8 6 7 eqeltrd ⊢ φ ∧ x ∈ A → F ⁡ x ∈ B
9 8 ralrimiva ⊢ φ → ∀ x ∈ A F ⁡ x ∈ B
10 1 9 jca ⊢ φ → F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
11 ffnfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
12 10 11 sylibr ⊢ φ → F : A ⟶ B
13 snex ⊢ A ∈ V
14 13 a1i ⊢ φ → A ∈ V
15 2 14 elmapd ⊢ φ → F ∈ B A ↔ F : A ⟶ B
16 12 15 mpbird ⊢ φ → F ∈ B A