Metamath Proof Explorer

Theorem elixpsn

Description: Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion elixpsn ⊢ A ∈ V → F ∈ ⨉ x ∈ A B ↔ ∃ y ∈ B F = A y

Proof

Step Hyp Ref Expression
1 sneq ⊢ z = A → z = A
2 1 ixpeq1d ⊢ z = A → ⨉ x ∈ z B = ⨉ x ∈ A B
3 2 eleq2d ⊢ z = A → F ∈ ⨉ x ∈ z B ↔ F ∈ ⨉ x ∈ A B
4 opeq1 ⊢ z = A → z y = A y
5 4 sneqd ⊢ z = A → z y = A y
6 5 eqeq2d ⊢ z = A → F = z y ↔ F = A y
7 6 rexbidv ⊢ z = A → ∃ y ∈ B F = z y ↔ ∃ y ∈ B F = A y
8 elex ⊢ F ∈ ⨉ x ∈ z B → F ∈ V
9 snex ⊢ z y ∈ V
10 eleq1 ⊢ F = z y → F ∈ V ↔ z y ∈ V
11 9 10 mpbiri ⊢ F = z y → F ∈ V
12 11 rexlimivw ⊢ ∃ y ∈ B F = z y → F ∈ V
13 eleq1 ⊢ w = F → w ∈ ⨉ x ∈ z B ↔ F ∈ ⨉ x ∈ z B
14 eqeq1 ⊢ w = F → w = z y ↔ F = z y
15 14 rexbidv ⊢ w = F → ∃ y ∈ B w = z y ↔ ∃ y ∈ B F = z y
16 vex ⊢ w ∈ V
17 16 elixp ⊢ w ∈ ⨉ x ∈ z B ↔ w Fn z ∧ ∀ x ∈ z w ⁡ x ∈ B
18 vex ⊢ z ∈ V
19 fveq2 ⊢ x = z → w ⁡ x = w ⁡ z
20 19 eleq1d ⊢ x = z → w ⁡ x ∈ B ↔ w ⁡ z ∈ B
21 18 20 ralsn ⊢ ∀ x ∈ z w ⁡ x ∈ B ↔ w ⁡ z ∈ B
22 21 anbi2i ⊢ w Fn z ∧ ∀ x ∈ z w ⁡ x ∈ B ↔ w Fn z ∧ w ⁡ z ∈ B
23 simpl ⊢ w Fn z ∧ w ⁡ z ∈ B → w Fn z
24 fveq2 ⊢ y = z → w ⁡ y = w ⁡ z
25 24 eleq1d ⊢ y = z → w ⁡ y ∈ B ↔ w ⁡ z ∈ B
26 18 25 ralsn ⊢ ∀ y ∈ z w ⁡ y ∈ B ↔ w ⁡ z ∈ B
27 26 bilanri ⊢ w Fn z ∧ w ⁡ z ∈ B → ∀ y ∈ z w ⁡ y ∈ B
28 ffnfv ⊢ w : z ⟶ B ↔ w Fn z ∧ ∀ y ∈ z w ⁡ y ∈ B
29 23 27 28 sylanbrc ⊢ w Fn z ∧ w ⁡ z ∈ B → w : z ⟶ B
30 18 fsn2 ⊢ w : z ⟶ B ↔ w ⁡ z ∈ B ∧ w = z w ⁡ z
31 29 30 sylib ⊢ w Fn z ∧ w ⁡ z ∈ B → w ⁡ z ∈ B ∧ w = z w ⁡ z
32 opeq2 ⊢ y = w ⁡ z → z y = z w ⁡ z
33 32 sneqd ⊢ y = w ⁡ z → z y = z w ⁡ z
34 33 rspceeqv ⊢ w ⁡ z ∈ B ∧ w = z w ⁡ z → ∃ y ∈ B w = z y
35 31 34 syl ⊢ w Fn z ∧ w ⁡ z ∈ B → ∃ y ∈ B w = z y
36 vex ⊢ y ∈ V
37 18 36 fvsn ⊢ z y ⁡ z = y
38 id ⊢ y ∈ B → y ∈ B
39 37 38 eqeltrid ⊢ y ∈ B → z y ⁡ z ∈ B
40 18 36 fnsn ⊢ z y Fn z
41 39 40 jctil ⊢ y ∈ B → z y Fn z ∧ z y ⁡ z ∈ B
42 fneq1 ⊢ w = z y → w Fn z ↔ z y Fn z
43 fveq1 ⊢ w = z y → w ⁡ z = z y ⁡ z
44 43 eleq1d ⊢ w = z y → w ⁡ z ∈ B ↔ z y ⁡ z ∈ B
45 42 44 anbi12d ⊢ w = z y → w Fn z ∧ w ⁡ z ∈ B ↔ z y Fn z ∧ z y ⁡ z ∈ B
46 41 45 syl5ibrcom ⊢ y ∈ B → w = z y → w Fn z ∧ w ⁡ z ∈ B
47 46 rexlimiv ⊢ ∃ y ∈ B w = z y → w Fn z ∧ w ⁡ z ∈ B
48 35 47 impbii ⊢ w Fn z ∧ w ⁡ z ∈ B ↔ ∃ y ∈ B w = z y
49 17 22 48 3bitri ⊢ w ∈ ⨉ x ∈ z B ↔ ∃ y ∈ B w = z y
50 13 15 49 vtoclbg ⊢ F ∈ V → F ∈ ⨉ x ∈ z B ↔ ∃ y ∈ B F = z y
51 8 12 50 pm5.21nii ⊢ F ∈ ⨉ x ∈ z B ↔ ∃ y ∈ B F = z y
52 3 7 51 vtoclbg ⊢ A ∈ V → F ∈ ⨉ x ∈ A B ↔ ∃ y ∈ B F = A y