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 dom B B A

Proof

Step Hyp Ref Expression
1 elex A dom B A V
2 snprc ¬ A V A =
3 reseq2 A = B A = B
4 res0 B =
5 3 4 syl6eq A = B A =
6 2 5 sylbi ¬ A V B A =
7 6 necon1ai B A A V
8 eleq1 x = A x dom B A dom B
9 sneq x = A x = A
10 9 reseq2d x = A B x = B A
11 10 neeq1d x = A B x B A
12 dfclel x y B p p = x y p B
13 12 exbii y x y B y p p = x y p B
14 vex x V
15 14 eldm2 x dom B y x y B
16 n0 B x p p B x
17 elres p B x z x y p = z y z y B
18 eleq1 p = z y p B z y B
19 18 pm5.32i p = z y p B p = z y z y B
20 opeq1 z = x z y = x y
21 20 eqeq2d z = x p = z y p = x y
22 21 anbi1d z = x p = z y p B p = x y p B
23 19 22 syl5bbr z = x p = z y z y B p = x y p B
24 23 exbidv z = x y p = z y z y B y p = x y p B
25 14 24 rexsn z x y p = z y z y B y p = x y p B
26 17 25 bitri p B x y p = x y p B
27 26 exbii p p B x p y p = x y p B
28 excom p y p = x y p B y p p = x y p B
29 16 27 28 3bitri B x y p p = x y p B
30 13 15 29 3bitr4i x dom B B x
31 8 11 30 vtoclbg A V A dom B B A
32 1 7 31 pm5.21nii A dom B B A