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 biimpri ⊢ w ⁡ z ∈ B → ∀ y ∈ z w ⁡ y ∈ B
28 27 adantl ⊢ w Fn z ∧ w ⁡ z ∈ B → ∀ y ∈ z w ⁡ y ∈ B
29 ffnfv ⊢ w : z ⟶ B ↔ w Fn z ∧ ∀ y ∈ z w ⁡ y ∈ B
30 23 28 29 sylanbrc ⊢ w Fn z ∧ w ⁡ z ∈ B → w : z ⟶ B
31 18 fsn2 ⊢ w : z ⟶ B ↔ w ⁡ z ∈ B ∧ w = z w ⁡ z
32 30 31 sylib ⊢ w Fn z ∧ w ⁡ z ∈ B → w ⁡ z ∈ B ∧ w = z w ⁡ z
33 opeq2 ⊢ y = w ⁡ z → z y = z w ⁡ z
34 33 sneqd ⊢ y = w ⁡ z → z y = z w ⁡ z
35 34 rspceeqv ⊢ w ⁡ z ∈ B ∧ w = z w ⁡ z → ∃ y ∈ B w = z y
36 32 35 syl ⊢ w Fn z ∧ w ⁡ z ∈ B → ∃ y ∈ B w = z y
37 vex ⊢ y ∈ V
38 18 37 fvsn ⊢ z y ⁡ z = y
39 id ⊢ y ∈ B → y ∈ B
40 38 39 eqeltrid ⊢ y ∈ B → z y ⁡ z ∈ B
41 18 37 fnsn ⊢ z y Fn z
42 40 41 jctil ⊢ y ∈ B → z y Fn z ∧ z y ⁡ z ∈ B
43 fneq1 ⊢ w = z y → w Fn z ↔ z y Fn z
44 fveq1 ⊢ w = z y → w ⁡ z = z y ⁡ z
45 44 eleq1d ⊢ w = z y → w ⁡ z ∈ B ↔ z y ⁡ z ∈ B
46 43 45 anbi12d ⊢ w = z y → w Fn z ∧ w ⁡ z ∈ B ↔ z y Fn z ∧ z y ⁡ z ∈ B
47 42 46 syl5ibrcom ⊢ y ∈ B → w = z y → w Fn z ∧ w ⁡ z ∈ B
48 47 rexlimiv ⊢ ∃ y ∈ B w = z y → w Fn z ∧ w ⁡ z ∈ B
49 36 48 impbii ⊢ w Fn z ∧ w ⁡ z ∈ B ↔ ∃ y ∈ B w = z y
50 17 22 49 3bitri ⊢ w ∈ ⨉ x ∈ z B ↔ ∃ y ∈ B w = z y
51 13 15 50 vtoclbg ⊢ F ∈ V → F ∈ ⨉ x ∈ z B ↔ ∃ y ∈ B F = z y
52 8 12 51 pm5.21nii ⊢ F ∈ ⨉ x ∈ z B ↔ ∃ y ∈ B F = z y
53 3 7 52 vtoclbg ⊢ A ∈ V → F ∈ ⨉ x ∈ A B ↔ ∃ y ∈ B F = A y