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

Metamath Proof Explorer

Theorem elfvmptrab

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

		Ref	Expression
	Hypotheses	elfvmptrab.f	$⊢ F = (x \in V ⟼ \{y \in M \| φ\})$
		elfvmptrab.v	$⊢ X \in V \to M \in V$
	Assertion	elfvmptrab	$⊢ Y \in F (X) \to (X \in V \land Y \in M)$

Proof

Step	Hyp	Ref	Expression
1		elfvmptrab.f	$⊢ F = (x \in V ⟼ \{y \in M \| φ\})$
2		elfvmptrab.v	$⊢ X \in V \to M \in V$
3		csbconstg	$⊢ x \in V \to ⦋ x / m ⦌ M = M$
4	3	eqcomd	$⊢ x \in V \to M = ⦋ x / m ⦌ M$
5		rabeq	$⊢ M = ⦋ x / m ⦌ M \to \{y \in M \| φ\} = \{y \in ⦋ x / m ⦌ M \| φ\}$
6	4 5	syl	$⊢ x \in V \to \{y \in M \| φ\} = \{y \in ⦋ x / m ⦌ M \| φ\}$
7	6	mpteq2ia	$⊢ (x \in V ⟼ \{y \in M \| φ\}) = (x \in V ⟼ \{y \in ⦋ x / m ⦌ M \| φ\})$
8	1 7	eqtri	$⊢ F = (x \in V ⟼ \{y \in ⦋ x / m ⦌ M \| φ\})$
9		csbconstg	$⊢ X \in V \to ⦋ X / m ⦌ M = M$
10	9 2	eqeltrd	$⊢ X \in V \to ⦋ X / m ⦌ M \in V$
11	8 10	elfvmptrab1w	$⊢ Y \in F (X) \to (X \in V \land Y \in ⦋ X / m ⦌ M)$
12	9	eleq2d	$⊢ X \in V \to (Y \in ⦋ X / m ⦌ M \leftrightarrow Y \in M)$
13	12	biimpd	$⊢ X \in V \to (Y \in ⦋ X / m ⦌ M \to Y \in M)$
14	13	imdistani	$⊢ (X \in V \land Y \in ⦋ X / m ⦌ M) \to (X \in V \land Y \in M)$
15	11 14	syl	$⊢ Y \in F (X) \to (X \in V \land Y \in M)$