Theorem fvmptrab

Description: Value of a function mapping a set to a class abstraction restricting a class depending on the argument of the function. More general version of fvmptrabfv , but relying on the fact that out-of-domain arguments evaluate to the empty set, which relies on set.mm's particular encoding. (Contributed by AV, 14-Feb-2022)

	Ref	Expression
Hypotheses	fvmptrab.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑀 ∣ 𝜑 } )
	fvmptrab.r	⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜓 ) )
	fvmptrab.s	⊢ ( 𝑥 = 𝑋 → 𝑀 = 𝑁 )
	fvmptrab.v	⊢ ( 𝑋 ∈ 𝑉 → 𝑁 ∈ V )
	fvmptrab.n	⊢ ( 𝑋 ∉ 𝑉 → 𝑁 = ∅ )
Assertion	fvmptrab	⊢ ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ 𝑁 ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		fvmptrab.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑀 ∣ 𝜑 } )
2		fvmptrab.r	⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜓 ) )
3		fvmptrab.s	⊢ ( 𝑥 = 𝑋 → 𝑀 = 𝑁 )
4		fvmptrab.v	⊢ ( 𝑋 ∈ 𝑉 → 𝑁 ∈ V )
5		fvmptrab.n	⊢ ( 𝑋 ∉ 𝑉 → 𝑁 = ∅ )
6	1	a1i	⊢ ( 𝑋 ∈ 𝑉 → 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑀 ∣ 𝜑 } ) )
7	3 2	rabeqbidv	⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ 𝑁 ∣ 𝜓 } )
8	7	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 = 𝑋 ) → { 𝑦 ∈ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ 𝑁 ∣ 𝜓 } )
9		id	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ 𝑉 )
10		eqid	⊢ { 𝑦 ∈ 𝑁 ∣ 𝜓 } = { 𝑦 ∈ 𝑁 ∣ 𝜓 }
11	10 4	rabexd	⊢ ( 𝑋 ∈ 𝑉 → { 𝑦 ∈ 𝑁 ∣ 𝜓 } ∈ V )
12	6 8 9 11	fvmptd	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ 𝑁 ∣ 𝜓 } )
13	1	fvmptndm	⊢ ( ¬ 𝑋 ∈ 𝑉 → ( 𝐹 ‘ 𝑋 ) = ∅ )
14		df-nel	⊢ ( 𝑋 ∉ 𝑉 ↔ ¬ 𝑋 ∈ 𝑉 )
15		rabeq	⊢ ( 𝑁 = ∅ → { 𝑦 ∈ 𝑁 ∣ 𝜓 } = { 𝑦 ∈ ∅ ∣ 𝜓 } )
16		rab0	⊢ { 𝑦 ∈ ∅ ∣ 𝜓 } = ∅
17	15 16	eqtr2di	⊢ ( 𝑁 = ∅ → ∅ = { 𝑦 ∈ 𝑁 ∣ 𝜓 } )
18	5 17	syl	⊢ ( 𝑋 ∉ 𝑉 → ∅ = { 𝑦 ∈ 𝑁 ∣ 𝜓 } )
19	14 18	sylbir	⊢ ( ¬ 𝑋 ∈ 𝑉 → ∅ = { 𝑦 ∈ 𝑁 ∣ 𝜓 } )
20	13 19	eqtrd	⊢ ( ¬ 𝑋 ∈ 𝑉 → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ 𝑁 ∣ 𝜓 } )
21	12 20	pm2.61i	⊢ ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ 𝑁 ∣ 𝜓 }