Theorem fnasrn

Description: A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	dfmpt.1	⊢ 𝐵 ∈ V
Assertion	fnasrn	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		dfmpt.1	⊢ 𝐵 ∈ V
2	1	dfmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ )
4	3	rnmpt	⊢ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ }
5		velsn	⊢ ( 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } ↔ 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ )
6	5	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ )
7	6	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ⟨ 𝑥 , 𝐵 ⟩ }
8	4 7	eqtr4i	⊢ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } }
9		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { ⟨ 𝑥 , 𝐵 ⟩ } }
10	8 9	eqtr4i	⊢ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ ) = ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
11	2 10	eqtr4i	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝐵 ⟩ )