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∈AB↔∃y∈BF=Ay

Proof

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