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

Metamath Proof Explorer

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