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

Metamath Proof Explorer

Theorem elmapd

Description: Deduction form of elmapg . (Contributed by BJ, 11-Apr-2020)

Ref Expression
Hypotheses elmapd.a ⊢ φ → A ∈ V
elmapd.b ⊢ φ → B ∈ W
Assertion elmapd ⊢ φ → C ∈ A B ↔ C : B ⟶ A

Proof

Step Hyp Ref Expression
1 elmapd.a ⊢ φ → A ∈ V
2 elmapd.b ⊢ φ → B ∈ W
3 elmapg ⊢ A ∈ V ∧ B ∈ W → C ∈ A B ↔ C : B ⟶ A
4 1 2 3 syl2anc ⊢ φ → C ∈ A B ↔ C : B ⟶ A