Metamath Proof Explorer


Theorem dibdmN

Description: Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibfn.b B = Base K
dibfn.l ˙ = K
dibfn.h H = LHyp K
dibfn.i I = DIsoB K W
Assertion dibdmN K V W H dom I = x B | x ˙ W

Proof

Step Hyp Ref Expression
1 dibfn.b B = Base K
2 dibfn.l ˙ = K
3 dibfn.h H = LHyp K
4 dibfn.i I = DIsoB K W
5 1 2 3 4 dibfnN K V W H I Fn x B | x ˙ W
6 5 fndmd K V W H dom I = x B | x ˙ W