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	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑀 ∣ 𝜑 } )
	elfvmptrab.v	⊢ ( 𝑋 ∈ 𝑉 → 𝑀 ∈ V )
Assertion	elfvmptrab	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		elfvmptrab.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑀 ∣ 𝜑 } )
2		elfvmptrab.v	⊢ ( 𝑋 ∈ 𝑉 → 𝑀 ∈ V )
3		csbconstg	⊢ ( 𝑥 ∈ 𝑉 → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = 𝑀 )
4	3	eqcomd	⊢ ( 𝑥 ∈ 𝑉 → 𝑀 = ⦋ 𝑥 / 𝑚 ⦌ 𝑀 )
5		rabeq	⊢ ( 𝑀 = ⦋ 𝑥 / 𝑚 ⦌ 𝑀 → { 𝑦 ∈ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
6	4 5	syl	⊢ ( 𝑥 ∈ 𝑉 → { 𝑦 ∈ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
7	6	mpteq2ia	⊢ ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑀 ∣ 𝜑 } ) = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
8	1 7	eqtri	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
9		csbconstg	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 = 𝑀 )
10	9 2	eqeltrd	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
11	8 10	elfvmptrab1w	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )
12	9	eleq2d	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ↔ 𝑌 ∈ 𝑀 ) )
13	12	biimpd	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 → 𝑌 ∈ 𝑀 ) )
14	13	imdistani	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑀 ) )
15	11 14	syl	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑀 ) )