# Metamath Proof Explorer

## Theorem elfvmptrab1

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elfvmptrab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

Ref Expression
Hypotheses elfvmptrab1.f
elfvmptrab1.v
Assertion elfvmptrab1

### Proof

Step Hyp Ref Expression
1 elfvmptrab1.f
2 elfvmptrab1.v
3 ne0i $⊢ Y ∈ F ⁡ X → F ⁡ X ≠ ∅$
4 ndmfv $⊢ ¬ X ∈ dom ⁡ F → F ⁡ X = ∅$
5 4 necon1ai $⊢ F ⁡ X ≠ ∅ → X ∈ dom ⁡ F$
6 1 dmmptss $⊢ dom ⁡ F ⊆ V$
7 6 sseli $⊢ X ∈ dom ⁡ F → X ∈ V$
8 rabexg
9 7 2 8 3syl
10 nfcv $⊢ Ⅎ _ x X$
11 nfsbc1v
12 nfcv $⊢ Ⅎ _ x M$
13 10 12 nfcsb
14 11 13 nfrab
15 csbeq1
16 sbceq1a
17 15 16 rabeqbidv
18 10 14 17 1 fvmptf
19 7 9 18 syl2anc
20 19 eleq2d
21 elrabi
22 7 21 anim12i
23 22 ex
24 20 23 sylbid
25 3 5 24 3syl
26 25 pm2.43i