Theorem elrnmpt1

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	rnmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		vex	⊢ 𝑥 ∈ V
3		id	⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
4		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
5	3 4	eleq12d	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) )
6		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
7	6	biantrud	⊢ ( 𝑥 = 𝑧 → ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ↔ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
8	5 7	bitr2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) )
9	8	equcoms	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) )
10	2 9	spcev	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
11		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) )
12		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 )
13		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
14	13	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴
15		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
16	15	nfeq2	⊢ Ⅎ 𝑥 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵
17	14 16	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
18	6	eqeq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
19	5 18	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
20	12 17 19	cbvexv1	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
21	11 20	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
22		eqeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↔ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
23	22	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
24	23	exbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ∃ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
25	21 24	bitrid	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
26	1	rnmpt	⊢ ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
27	25 26	elab2g	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
28	10 27	syl5ibr	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ ran 𝐹 ) )
29	28	impcom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ran 𝐹 )