# Metamath Proof Explorer

## Theorem elfvmptrab1w

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. Version of elfvmptrab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypotheses elfvmptrab1w.f
elfvmptrab1w.v
Assertion elfvmptrab1w

### Proof

Step Hyp Ref Expression
1 elfvmptrab1w.f
2 elfvmptrab1w.v
3 elfvdm ${⊢}{Y}\in {F}\left({X}\right)\to {X}\in \mathrm{dom}{F}$
4 1 dmmptss ${⊢}\mathrm{dom}{F}\subseteq {V}$
5 4 sseli ${⊢}{X}\in \mathrm{dom}{F}\to {X}\in {V}$
6 rabexg
7 5 2 6 3syl
8 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{X}$
9 nfsbc1v
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{M}$
11 8 10 nfcsbw
12 9 11 nfrabw
13 csbeq1
14 sbceq1a
15 13 14 rabeqbidv
16 8 12 15 1 fvmptf
17 5 7 16 syl2anc
18 17 eleq2d
19 elrabi
20 5 19 anim12i
21 20 ex
22 18 21 sylbid
23 3 22 mpcom