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

Metamath Proof Explorer

Theorem fvmptrabfv

Description: Value of a function mapping a set to a class abstraction restricting the value of another function. (Contributed by AV, 18-Feb-2022)

Ref Expression
Hypotheses fvmptrabfv.f ⊢ 𝐹 = ( 𝑥 ∈ V ↦ { 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ∣ 𝜑 } )
fvmptrabfv.r ⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜓 ) )
Assertion fvmptrabfv ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 }

Proof

Step Hyp Ref Expression
1 fvmptrabfv.f ⊢ 𝐹 = ( 𝑥 ∈ V ↦ { 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ∣ 𝜑 } )
2 fvmptrabfv.r ⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜓 ) )
3 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
4 3 2 rabeqbidv ⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ ( 𝐺 ‘ 𝑥 ) ∣ 𝜑 } = { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 } )
5 fvex ⊢ ( 𝐺 ‘ 𝑋 ) ∈ V
6 5 rabex ⊢ { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 } ∈ V
7 4 1 6 fvmpt ⊢ ( 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 } )
8 fvprc ⊢ ( ¬ 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = ∅ )
9 fvprc ⊢ ( ¬ 𝑋 ∈ V → ( 𝐺 ‘ 𝑋 ) = ∅ )
10 9 rabeqdv ⊢ ( ¬ 𝑋 ∈ V → { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 } = { 𝑦 ∈ ∅ ∣ 𝜓 } )
11 rab0 ⊢ { 𝑦 ∈ ∅ ∣ 𝜓 } = ∅
12 10 11 eqtr2di ⊢ ( ¬ 𝑋 ∈ V → ∅ = { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 } )
13 8 12 eqtrd ⊢ ( ¬ 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 } )
14 7 13 pm2.61i ⊢ ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 }