Theorem elabrex

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014)

	Ref	Expression
Hypothesis	elabrex.1	⊢ 𝐵 ∈ V
Assertion	elabrex	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		elabrex.1	⊢ 𝐵 ∈ V
2		tru	⊢ ⊤
3		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
4	3	equcoms	⊢ ( 𝑧 = 𝑥 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
5		trud	⊢ ( 𝑧 = 𝑥 → ⊤ )
6	4 5	2thd	⊢ ( 𝑧 = 𝑥 → ( 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↔ ⊤ ) )
7	6	rspcev	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ⊤ ) → ∃ 𝑧 ∈ 𝐴 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
8	2 7	mpan2	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
9		eqeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↔ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
10	9	rexbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↔ ∃ 𝑧 ∈ 𝐴 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
11	1 10	elab	⊢ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 } ↔ ∃ 𝑧 ∈ 𝐴 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
12	8 11	sylibr	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 } )
13		nfv	⊢ Ⅎ 𝑧 𝑦 = 𝐵
14		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
15	14	nfeq2	⊢ Ⅎ 𝑥 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵
16	3	eqeq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
17	13 15 16	cbvrexw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
18	17	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 }
19	12 18	eleqtrrdi	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )