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 ⊢ F = x ∈ V ⟼ y ∈ G ⁡ x | φ
fvmptrabfv.r ⊢ x = X → φ ↔ ψ
Assertion fvmptrabfv ⊢ F ⁡ X = y ∈ G ⁡ X | ψ

Proof

Step Hyp Ref Expression
1 fvmptrabfv.f ⊢ F = x ∈ V ⟼ y ∈ G ⁡ x | φ
2 fvmptrabfv.r ⊢ x = X → φ ↔ ψ
3 fveq2 ⊢ x = X → G ⁡ x = G ⁡ X
4 3 2 rabeqbidv ⊢ x = X → y ∈ G ⁡ x | φ = y ∈ G ⁡ X | ψ
5 fvex ⊢ G ⁡ X ∈ V
6 5 rabex ⊢ y ∈ G ⁡ X | ψ ∈ V
7 4 1 6 fvmpt ⊢ X ∈ V → F ⁡ X = y ∈ G ⁡ X | ψ
8 fvprc ⊢ ¬ X ∈ V → F ⁡ X = ∅
9 fvprc ⊢ ¬ X ∈ V → G ⁡ X = ∅
10 9 rabeqdv ⊢ ¬ X ∈ V → y ∈ G ⁡ X | ψ = y ∈ ∅ | ψ
11 rab0 ⊢ y ∈ ∅ | ψ = ∅
12 10 11 eqtr2di ⊢ ¬ X ∈ V → ∅ = y ∈ G ⁡ X | ψ
13 8 12 eqtrd ⊢ ¬ X ∈ V → F ⁡ X = y ∈ G ⁡ X | ψ
14 7 13 pm2.61i ⊢ F ⁡ X = y ∈ G ⁡ X | ψ