Theorem elabrexg

Description: Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elabrexg	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )

Proof

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