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 ⊢ B ∈ V
Assertion elabrex ⊢ x ∈ A → B ∈ y | ∃ x ∈ A y = B

Proof

Step Hyp Ref Expression
1 elabrex.1 ⊢ B ∈ V
2 tru ⊢ ⊤
3 csbeq1a ⊢ x = z → B = ⦋ z / x⦌ B
4 3 equcoms ⊢ z = x → B = ⦋ z / x⦌ B
5 trud ⊢ z = x → ⊤
6 4 5 2thd ⊢ z = x → B = ⦋ z / x⦌ B ↔ ⊤
7 6 rspcev ⊢ x ∈ A ∧ ⊤ → ∃ z ∈ A B = ⦋ z / x⦌ B
8 2 7 mpan2 ⊢ x ∈ A → ∃ z ∈ A B = ⦋ z / x⦌ B
9 eqeq1 ⊢ y = B → y = ⦋ z / x⦌ B ↔ B = ⦋ z / x⦌ B
10 9 rexbidv ⊢ y = B → ∃ z ∈ A y = ⦋ z / x⦌ B ↔ ∃ z ∈ A B = ⦋ z / x⦌ B
11 1 10 elab ⊢ B ∈ y | ∃ z ∈ A y = ⦋ z / x⦌ B ↔ ∃ z ∈ A B = ⦋ z / x⦌ B
12 8 11 sylibr ⊢ x ∈ A → B ∈ y | ∃ z ∈ A y = ⦋ z / x⦌ B
13 nfv ⊢ Ⅎ z y = B
14 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ B
15 14 nfeq2 ⊢ Ⅎ x y = ⦋ z / x⦌ B
16 3 eqeq2d ⊢ x = z → y = B ↔ y = ⦋ z / x⦌ B
17 13 15 16 cbvrexw ⊢ ∃ x ∈ A y = B ↔ ∃ z ∈ A y = ⦋ z / x⦌ B
18 17 abbii ⊢ y | ∃ x ∈ A y = B = y | ∃ z ∈ A y = ⦋ z / x⦌ B
19 12 18 eleqtrrdi ⊢ x ∈ A → B ∈ y | ∃ x ∈ A y = B