# Metamath Proof Explorer

## Theorem eldm3

Description: Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017)

Ref Expression
Assertion eldm3 ${⊢}{A}\in \mathrm{dom}{B}↔{{B}↾}_{\left\{{A}\right\}}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in \mathrm{dom}{B}\to {A}\in \mathrm{V}$
2 snprc ${⊢}¬{A}\in \mathrm{V}↔\left\{{A}\right\}=\varnothing$
3 reseq2 ${⊢}\left\{{A}\right\}=\varnothing \to {{B}↾}_{\left\{{A}\right\}}={{B}↾}_{\varnothing }$
4 res0 ${⊢}{{B}↾}_{\varnothing }=\varnothing$
5 3 4 syl6eq ${⊢}\left\{{A}\right\}=\varnothing \to {{B}↾}_{\left\{{A}\right\}}=\varnothing$
6 2 5 sylbi ${⊢}¬{A}\in \mathrm{V}\to {{B}↾}_{\left\{{A}\right\}}=\varnothing$
7 6 necon1ai ${⊢}{{B}↾}_{\left\{{A}\right\}}\ne \varnothing \to {A}\in \mathrm{V}$
8 eleq1 ${⊢}{x}={A}\to \left({x}\in \mathrm{dom}{B}↔{A}\in \mathrm{dom}{B}\right)$
9 sneq ${⊢}{x}={A}\to \left\{{x}\right\}=\left\{{A}\right\}$
10 9 reseq2d ${⊢}{x}={A}\to {{B}↾}_{\left\{{x}\right\}}={{B}↾}_{\left\{{A}\right\}}$
11 10 neeq1d ${⊢}{x}={A}\to \left({{B}↾}_{\left\{{x}\right\}}\ne \varnothing ↔{{B}↾}_{\left\{{A}\right\}}\ne \varnothing \right)$
12 dfclel ${⊢}⟨{x},{y}⟩\in {B}↔\exists {p}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)$
13 12 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {B}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)$
14 vex ${⊢}{x}\in \mathrm{V}$
15 14 eldm2 ${⊢}{x}\in \mathrm{dom}{B}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {B}$
16 n0 ${⊢}{{B}↾}_{\left\{{x}\right\}}\ne \varnothing ↔\exists {p}\phantom{\rule{.4em}{0ex}}{p}\in \left({{B}↾}_{\left\{{x}\right\}}\right)$
17 elres ${⊢}{p}\in \left({{B}↾}_{\left\{{x}\right\}}\right)↔\exists {z}\in \left\{{x}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{z},{y}⟩\wedge ⟨{z},{y}⟩\in {B}\right)$
18 eleq1 ${⊢}{p}=⟨{z},{y}⟩\to \left({p}\in {B}↔⟨{z},{y}⟩\in {B}\right)$
19 18 pm5.32i ${⊢}\left({p}=⟨{z},{y}⟩\wedge {p}\in {B}\right)↔\left({p}=⟨{z},{y}⟩\wedge ⟨{z},{y}⟩\in {B}\right)$
20 opeq1 ${⊢}{z}={x}\to ⟨{z},{y}⟩=⟨{x},{y}⟩$
21 20 eqeq2d ${⊢}{z}={x}\to \left({p}=⟨{z},{y}⟩↔{p}=⟨{x},{y}⟩\right)$
22 21 anbi1d ${⊢}{z}={x}\to \left(\left({p}=⟨{z},{y}⟩\wedge {p}\in {B}\right)↔\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)\right)$
23 19 22 syl5bbr ${⊢}{z}={x}\to \left(\left({p}=⟨{z},{y}⟩\wedge ⟨{z},{y}⟩\in {B}\right)↔\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)\right)$
24 23 exbidv ${⊢}{z}={x}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{z},{y}⟩\wedge ⟨{z},{y}⟩\in {B}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)\right)$
25 14 24 rexsn ${⊢}\exists {z}\in \left\{{x}\right\}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{z},{y}⟩\wedge ⟨{z},{y}⟩\in {B}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)$
26 17 25 bitri ${⊢}{p}\in \left({{B}↾}_{\left\{{x}\right\}}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)$
27 26 exbii ${⊢}\exists {p}\phantom{\rule{.4em}{0ex}}{p}\in \left({{B}↾}_{\left\{{x}\right\}}\right)↔\exists {p}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)$
28 excom ${⊢}\exists {p}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)$
29 16 27 28 3bitri ${⊢}{{B}↾}_{\left\{{x}\right\}}\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{x},{y}⟩\wedge {p}\in {B}\right)$
30 13 15 29 3bitr4i ${⊢}{x}\in \mathrm{dom}{B}↔{{B}↾}_{\left\{{x}\right\}}\ne \varnothing$
31 8 11 30 vtoclbg ${⊢}{A}\in \mathrm{V}\to \left({A}\in \mathrm{dom}{B}↔{{B}↾}_{\left\{{A}\right\}}\ne \varnothing \right)$
32 1 7 31 pm5.21nii ${⊢}{A}\in \mathrm{dom}{B}↔{{B}↾}_{\left\{{A}\right\}}\ne \varnothing$