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