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	⊢ ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ( 𝐺 ‘ 𝑋 ) ∣ 𝜓 }