Metamath Proof Explorer

Theorem elrnmpt1

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis rnmpt.1 ⊢ F = x ∈ A ⟼ B
Assertion elrnmpt1 ⊢ x ∈ A ∧ B ∈ V → B ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 rnmpt.1 ⊢ F = x ∈ A ⟼ B
2 vex ⊢ x ∈ V
3 id ⊢ x = z → x = z
4 csbeq1a ⊢ x = z → A = ⦋ z / x⦌ A
5 3 4 eleq12d ⊢ x = z → x ∈ A ↔ z ∈ ⦋ z / x⦌ A
6 csbeq1a ⊢ x = z → B = ⦋ z / x⦌ B
7 6 biantrud ⊢ x = z → z ∈ ⦋ z / x⦌ A ↔ z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B
8 5 7 bitr2d ⊢ x = z → z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B ↔ x ∈ A
9 8 equcoms ⊢ z = x → z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B ↔ x ∈ A
10 2 9 spcev ⊢ x ∈ A → ∃ z z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B
11 df-rex ⊢ ∃ x ∈ A y = B ↔ ∃ x x ∈ A ∧ y = B
12 nfv ⊢ Ⅎ z x ∈ A ∧ y = B
13 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ A
14 13 nfcri ⊢ Ⅎ x z ∈ ⦋ z / x⦌ A
15 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ B
16 15 nfeq2 ⊢ Ⅎ x y = ⦋ z / x⦌ B
17 14 16 nfan ⊢ Ⅎ x z ∈ ⦋ z / x⦌ A ∧ y = ⦋ z / x⦌ B
18 6 eqeq2d ⊢ x = z → y = B ↔ y = ⦋ z / x⦌ B
19 5 18 anbi12d ⊢ x = z → x ∈ A ∧ y = B ↔ z ∈ ⦋ z / x⦌ A ∧ y = ⦋ z / x⦌ B
20 12 17 19 cbvexv1 ⊢ ∃ x x ∈ A ∧ y = B ↔ ∃ z z ∈ ⦋ z / x⦌ A ∧ y = ⦋ z / x⦌ B
21 11 20 bitri ⊢ ∃ x ∈ A y = B ↔ ∃ z z ∈ ⦋ z / x⦌ A ∧ y = ⦋ z / x⦌ B
22 eqeq1 ⊢ y = B → y = ⦋ z / x⦌ B ↔ B = ⦋ z / x⦌ B
23 22 anbi2d ⊢ y = B → z ∈ ⦋ z / x⦌ A ∧ y = ⦋ z / x⦌ B ↔ z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B
24 23 exbidv ⊢ y = B → ∃ z z ∈ ⦋ z / x⦌ A ∧ y = ⦋ z / x⦌ B ↔ ∃ z z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B
25 21 24 bitrid ⊢ y = B → ∃ x ∈ A y = B ↔ ∃ z z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B
26 1 rnmpt ⊢ ran ⁡ F = y | ∃ x ∈ A y = B
27 25 26 elab2g ⊢ B ∈ V → B ∈ ran ⁡ F ↔ ∃ z z ∈ ⦋ z / x⦌ A ∧ B = ⦋ z / x⦌ B
28 10 27 imbitrrid ⊢ B ∈ V → x ∈ A → B ∈ ran ⁡ F
29 28 impcom ⊢ x ∈ A ∧ B ∈ V → B ∈ ran ⁡ F