This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Hypotheses elfvmptrab1w.f ⊢ F = x ∈ V ⟼ y ∈ ⦋ x / m⦌ M | φ
elfvmptrab1w.v ⊢ X ∈ V → ⦋ X / m⦌ M ∈ V
Assertion elfvmptrab1w ⊢ Y ∈ F ⁡ X → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M

Proof

Step Hyp Ref Expression
1 elfvmptrab1w.f ⊢ F = x ∈ V ⟼ y ∈ ⦋ x / m⦌ M | φ
2 elfvmptrab1w.v ⊢ X ∈ V → ⦋ X / m⦌ M ∈ V
3 elfvdm ⊢ Y ∈ F ⁡ X → X ∈ dom ⁡ F
4 1 dmmptss ⊢ dom ⁡ F ⊆ V
5 4 sseli ⊢ X ∈ dom ⁡ F → X ∈ V
6 rabexg ⊢ ⦋ X / m⦌ M ∈ V → y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ ∈ V
7 5 2 6 3syl ⊢ X ∈ dom ⁡ F → y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ ∈ V
8 nfcv ⊢ Ⅎ _ x X
9 nfsbc1v ⊢ Ⅎ x [˙X / x]˙ φ
10 nfcv ⊢ Ⅎ _ x M
11 8 10 nfcsbw ⊢ Ⅎ _ x ⦋ X / m⦌ M
12 9 11 nfrabw ⊢ Ⅎ _ x y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
13 csbeq1 ⊢ x = X → ⦋ x / m⦌ M = ⦋ X / m⦌ M
14 sbceq1a ⊢ x = X → φ ↔ [˙X / x]˙ φ
15 13 14 rabeqbidv ⊢ x = X → y ∈ ⦋ x / m⦌ M | φ = y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
16 8 12 15 1 fvmptf ⊢ X ∈ V ∧ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ ∈ V → F ⁡ X = y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
17 5 7 16 syl2anc ⊢ X ∈ dom ⁡ F → F ⁡ X = y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
18 17 eleq2d ⊢ X ∈ dom ⁡ F → Y ∈ F ⁡ X ↔ Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
19 elrabi ⊢ Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ → Y ∈ ⦋ X / m⦌ M
20 5 19 anim12i ⊢ X ∈ dom ⁡ F ∧ Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M
21 20 ex ⊢ X ∈ dom ⁡ F → Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M
22 18 21 sylbid ⊢ X ∈ dom ⁡ F → Y ∈ F ⁡ X → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M
23 3 22 mpcom ⊢ Y ∈ F ⁡ X → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M