This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Relations dmmptg
Description: The domain of the mapping operation is the stated domain, if the
function value is always a set. (Contributed by Mario Carneiro , 9-Feb-2013) (Revised by Mario Carneiro , 14-Sep-2013)
Ref
Expression
Assertion
dmmptg ⊢ ∀ x ∈ A B ∈ V → dom x ∈ A ⟼ B = A
Proof
Step
Hyp
Ref
Expression
1
eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
2
1
dmmpt ⊢ dom x ∈ A ⟼ B = x ∈ A | B ∈ V
3
elex ⊢ B ∈ V → B ∈ V
4
3
ralimi ⊢ ∀ x ∈ A B ∈ V → ∀ x ∈ A B ∈ V
5
rabid2 ⊢ A = x ∈ A | B ∈ V ↔ ∀ x ∈ A B ∈ V
6
4 5
sylibr ⊢ ∀ x ∈ A B ∈ V → A = x ∈ A | B ∈ V
7
2 6
eqtr4id ⊢ ∀ x ∈ A B ∈ V → dom x ∈ A ⟼ B = A