# 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}\in {V}\to \left({F}\in \underset{{x}\in \left\{{A}\right\}}{⨉}{B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{A},{y}⟩\right\}\right)$

### Proof

Step Hyp Ref Expression
1 sneq ${⊢}{z}={A}\to \left\{{z}\right\}=\left\{{A}\right\}$
2 1 ixpeq1d ${⊢}{z}={A}\to \underset{{x}\in \left\{{z}\right\}}{⨉}{B}=\underset{{x}\in \left\{{A}\right\}}{⨉}{B}$
3 2 eleq2d ${⊢}{z}={A}\to \left({F}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}↔{F}\in \underset{{x}\in \left\{{A}\right\}}{⨉}{B}\right)$
4 opeq1 ${⊢}{z}={A}\to ⟨{z},{y}⟩=⟨{A},{y}⟩$
5 4 sneqd ${⊢}{z}={A}\to \left\{⟨{z},{y}⟩\right\}=\left\{⟨{A},{y}⟩\right\}$
6 5 eqeq2d ${⊢}{z}={A}\to \left({F}=\left\{⟨{z},{y}⟩\right\}↔{F}=\left\{⟨{A},{y}⟩\right\}\right)$
7 6 rexbidv ${⊢}{z}={A}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{z},{y}⟩\right\}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{A},{y}⟩\right\}\right)$
8 elex ${⊢}{F}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}\to {F}\in \mathrm{V}$
9 snex ${⊢}\left\{⟨{z},{y}⟩\right\}\in \mathrm{V}$
10 eleq1 ${⊢}{F}=\left\{⟨{z},{y}⟩\right\}\to \left({F}\in \mathrm{V}↔\left\{⟨{z},{y}⟩\right\}\in \mathrm{V}\right)$
11 9 10 mpbiri ${⊢}{F}=\left\{⟨{z},{y}⟩\right\}\to {F}\in \mathrm{V}$
12 11 rexlimivw ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{z},{y}⟩\right\}\to {F}\in \mathrm{V}$
13 eleq1 ${⊢}{w}={F}\to \left({w}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}↔{F}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}\right)$
14 eqeq1 ${⊢}{w}={F}\to \left({w}=\left\{⟨{z},{y}⟩\right\}↔{F}=\left\{⟨{z},{y}⟩\right\}\right)$
15 14 rexbidv ${⊢}{w}={F}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}=\left\{⟨{z},{y}⟩\right\}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{z},{y}⟩\right\}\right)$
16 vex ${⊢}{w}\in \mathrm{V}$
17 16 elixp ${⊢}{w}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}↔\left({w}Fn\left\{{z}\right\}\wedge \forall {x}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}{w}\left({x}\right)\in {B}\right)$
18 vex ${⊢}{z}\in \mathrm{V}$
19 fveq2 ${⊢}{x}={z}\to {w}\left({x}\right)={w}\left({z}\right)$
20 19 eleq1d ${⊢}{x}={z}\to \left({w}\left({x}\right)\in {B}↔{w}\left({z}\right)\in {B}\right)$
21 18 20 ralsn ${⊢}\forall {x}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}{w}\left({x}\right)\in {B}↔{w}\left({z}\right)\in {B}$
22 21 anbi2i ${⊢}\left({w}Fn\left\{{z}\right\}\wedge \forall {x}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}{w}\left({x}\right)\in {B}\right)↔\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)$
23 simpl ${⊢}\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)\to {w}Fn\left\{{z}\right\}$
24 fveq2 ${⊢}{y}={z}\to {w}\left({y}\right)={w}\left({z}\right)$
25 24 eleq1d ${⊢}{y}={z}\to \left({w}\left({y}\right)\in {B}↔{w}\left({z}\right)\in {B}\right)$
26 18 25 ralsn ${⊢}\forall {y}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}{w}\left({y}\right)\in {B}↔{w}\left({z}\right)\in {B}$
27 26 biimpri ${⊢}{w}\left({z}\right)\in {B}\to \forall {y}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}{w}\left({y}\right)\in {B}$
28 27 adantl ${⊢}\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)\to \forall {y}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}{w}\left({y}\right)\in {B}$
29 ffnfv ${⊢}{w}:\left\{{z}\right\}⟶{B}↔\left({w}Fn\left\{{z}\right\}\wedge \forall {y}\in \left\{{z}\right\}\phantom{\rule{.4em}{0ex}}{w}\left({y}\right)\in {B}\right)$
30 23 28 29 sylanbrc ${⊢}\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)\to {w}:\left\{{z}\right\}⟶{B}$
31 18 fsn2 ${⊢}{w}:\left\{{z}\right\}⟶{B}↔\left({w}\left({z}\right)\in {B}\wedge {w}=\left\{⟨{z},{w}\left({z}\right)⟩\right\}\right)$
32 30 31 sylib ${⊢}\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)\to \left({w}\left({z}\right)\in {B}\wedge {w}=\left\{⟨{z},{w}\left({z}\right)⟩\right\}\right)$
33 opeq2 ${⊢}{y}={w}\left({z}\right)\to ⟨{z},{y}⟩=⟨{z},{w}\left({z}\right)⟩$
34 33 sneqd ${⊢}{y}={w}\left({z}\right)\to \left\{⟨{z},{y}⟩\right\}=\left\{⟨{z},{w}\left({z}\right)⟩\right\}$
35 34 rspceeqv ${⊢}\left({w}\left({z}\right)\in {B}\wedge {w}=\left\{⟨{z},{w}\left({z}\right)⟩\right\}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}=\left\{⟨{z},{y}⟩\right\}$
36 32 35 syl ${⊢}\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}=\left\{⟨{z},{y}⟩\right\}$
37 vex ${⊢}{y}\in \mathrm{V}$
38 18 37 fvsn ${⊢}\left\{⟨{z},{y}⟩\right\}\left({z}\right)={y}$
39 id ${⊢}{y}\in {B}\to {y}\in {B}$
40 38 39 eqeltrid ${⊢}{y}\in {B}\to \left\{⟨{z},{y}⟩\right\}\left({z}\right)\in {B}$
41 18 37 fnsn ${⊢}\left\{⟨{z},{y}⟩\right\}Fn\left\{{z}\right\}$
42 40 41 jctil ${⊢}{y}\in {B}\to \left(\left\{⟨{z},{y}⟩\right\}Fn\left\{{z}\right\}\wedge \left\{⟨{z},{y}⟩\right\}\left({z}\right)\in {B}\right)$
43 fneq1 ${⊢}{w}=\left\{⟨{z},{y}⟩\right\}\to \left({w}Fn\left\{{z}\right\}↔\left\{⟨{z},{y}⟩\right\}Fn\left\{{z}\right\}\right)$
44 fveq1 ${⊢}{w}=\left\{⟨{z},{y}⟩\right\}\to {w}\left({z}\right)=\left\{⟨{z},{y}⟩\right\}\left({z}\right)$
45 44 eleq1d ${⊢}{w}=\left\{⟨{z},{y}⟩\right\}\to \left({w}\left({z}\right)\in {B}↔\left\{⟨{z},{y}⟩\right\}\left({z}\right)\in {B}\right)$
46 43 45 anbi12d ${⊢}{w}=\left\{⟨{z},{y}⟩\right\}\to \left(\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)↔\left(\left\{⟨{z},{y}⟩\right\}Fn\left\{{z}\right\}\wedge \left\{⟨{z},{y}⟩\right\}\left({z}\right)\in {B}\right)\right)$
47 42 46 syl5ibrcom ${⊢}{y}\in {B}\to \left({w}=\left\{⟨{z},{y}⟩\right\}\to \left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)\right)$
48 47 rexlimiv ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}=\left\{⟨{z},{y}⟩\right\}\to \left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)$
49 36 48 impbii ${⊢}\left({w}Fn\left\{{z}\right\}\wedge {w}\left({z}\right)\in {B}\right)↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}=\left\{⟨{z},{y}⟩\right\}$
50 17 22 49 3bitri ${⊢}{w}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}=\left\{⟨{z},{y}⟩\right\}$
51 13 15 50 vtoclbg ${⊢}{F}\in \mathrm{V}\to \left({F}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{z},{y}⟩\right\}\right)$
52 8 12 51 pm5.21nii ${⊢}{F}\in \underset{{x}\in \left\{{z}\right\}}{⨉}{B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{z},{y}⟩\right\}$
53 3 7 52 vtoclbg ${⊢}{A}\in {V}\to \left({F}\in \underset{{x}\in \left\{{A}\right\}}{⨉}{B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{A},{y}⟩\right\}\right)$