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

Metamath Proof Explorer

Theorem sloteq

Description: Equality theorem for the Slot construction. The converse holds if A (or B ) is a set. (Contributed by BJ, 27-Dec-2021)

Ref Expression
Assertion sloteq ⊢ A = B → Slot A = Slot B

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ A = B → f ⁡ A = f ⁡ B
2 1 mpteq2dv ⊢ A = B → f ∈ V ⟼ f ⁡ A = f ∈ V ⟼ f ⁡ B
3 df-slot ⊢ Slot A = f ∈ V ⟼ f ⁡ A
4 df-slot ⊢ Slot B = f ∈ V ⟼ f ⁡ B
5 2 3 4 3eqtr4g ⊢ A = B → Slot A = Slot B