Metamath Proof Explorer

Theorem dmmptdff

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses dmmptdff.x ⊢ Ⅎ x φ
dmmptdff.1 ⊢ Ⅎ _ x B
dmmptdff.a ⊢ A = x ∈ B ⟼ C
dmmptdff.c ⊢ φ ∧ x ∈ B → C ∈ V
Assertion dmmptdff ⊢ φ → dom ⁡ A = B

Proof

Step Hyp Ref Expression
1 dmmptdff.x ⊢ Ⅎ x φ
2 dmmptdff.1 ⊢ Ⅎ _ x B
3 dmmptdff.a ⊢ A = x ∈ B ⟼ C
4 dmmptdff.c ⊢ φ ∧ x ∈ B → C ∈ V
5 3 dmmpt ⊢ dom ⁡ A = x ∈ B | C ∈ V
6 4 elexd ⊢ φ ∧ x ∈ B → C ∈ V
7 1 6 ralrimia ⊢ φ → ∀ x ∈ B C ∈ V
8 2 rabid2f ⊢ B = x ∈ B | C ∈ V ↔ ∀ x ∈ B C ∈ V
9 7 8 sylibr ⊢ φ → B = x ∈ B | C ∈ V
10 5 9 eqtr4id ⊢ φ → dom ⁡ A = B