This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )