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

Metamath Proof Explorer

Theorem elmapdd

Description: Deduction associated with elmapd . (Contributed by SN, 29-Jul-2024)

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

Proof

Step Hyp Ref Expression
1 elmapdd.a ⊢ φ → A ∈ V
2 elmapdd.b ⊢ φ → B ∈ W
3 elmapdd.c ⊢ φ → C : B ⟶ A
4 1 2 elmapd ⊢ φ → C ∈ A B ↔ C : B ⟶ A
5 3 4 mpbird ⊢ φ → C ∈ A B