Theorem imassmpt

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	imassmpt.1	⊢ Ⅎ 𝑥 𝜑
	imassmpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∈ 𝑉 )
	imassmpt.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	imassmpt	⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		imassmpt.1	⊢ Ⅎ 𝑥 𝜑
2		imassmpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∈ 𝑉 )
3		imassmpt.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4		df-ima	⊢ ( 𝐹 “ 𝐶 ) = ran ( 𝐹 ↾ 𝐶 )
5	3	reseq1i	⊢ ( 𝐹 ↾ 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 )
6		resmpt3	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
7	5 6	eqtri	⊢ ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
8	7	rneqi	⊢ ran ( 𝐹 ↾ 𝐶 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
9	4 8	eqtri	⊢ ( 𝐹 “ 𝐶 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
10	9	sseq1i	⊢ ( ( 𝐹 “ 𝐶 ) ⊆ 𝐷 ↔ ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 ) ⊆ 𝐷 )
11		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
12	1 11 2	rnmptssbi	⊢ ( 𝜑 → ( ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ∈ 𝐷 ) )
13	10 12	syl5bb	⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ∈ 𝐷 ) )