Metamath Proof Explorer


Theorem dfdm5

Description: Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfdm5 dom A = 1 st V × V A

Proof

Step Hyp Ref Expression
1 excom y p z p = z y p 1 st x p A p y z p = z y p 1 st x p A
2 opex z y V
3 breq1 p = z y p 1 st x z y 1 st x
4 eleq1 p = z y p A z y A
5 3 4 anbi12d p = z y p 1 st x p A z y 1 st x z y A
6 vex z V
7 vex y V
8 6 7 br1steq z y 1 st x x = z
9 equcom x = z z = x
10 8 9 bitri z y 1 st x z = x
11 10 anbi1i z y 1 st x z y A z = x z y A
12 5 11 bitrdi p = z y p 1 st x p A z = x z y A
13 2 12 ceqsexv p p = z y p 1 st x p A z = x z y A
14 13 exbii z p p = z y p 1 st x p A z z = x z y A
15 excom z p p = z y p 1 st x p A p z p = z y p 1 st x p A
16 vex x V
17 opeq1 z = x z y = x y
18 17 eleq1d z = x z y A x y A
19 16 18 ceqsexv z z = x z y A x y A
20 14 15 19 3bitr3ri x y A p z p = z y p 1 st x p A
21 20 exbii y x y A y p z p = z y p 1 st x p A
22 ancom p A p 1 st V × V x p 1 st V × V x p A
23 anass y z p = z y p 1 st x p A y z p = z y p 1 st x p A
24 16 brresi p 1 st V × V x p V × V p 1 st x
25 elvv p V × V z y p = z y
26 excom z y p = z y y z p = z y
27 25 26 bitri p V × V y z p = z y
28 27 anbi1i p V × V p 1 st x y z p = z y p 1 st x
29 24 28 bitri p 1 st V × V x y z p = z y p 1 st x
30 29 anbi1i p 1 st V × V x p A y z p = z y p 1 st x p A
31 19.41vv y z p = z y p 1 st x p A y z p = z y p 1 st x p A
32 23 30 31 3bitr4i p 1 st V × V x p A y z p = z y p 1 st x p A
33 22 32 bitri p A p 1 st V × V x y z p = z y p 1 st x p A
34 33 exbii p p A p 1 st V × V x p y z p = z y p 1 st x p A
35 1 21 34 3bitr4i y x y A p p A p 1 st V × V x
36 16 eldm2 x dom A y x y A
37 16 elima2 x 1 st V × V A p p A p 1 st V × V x
38 35 36 37 3bitr4i x dom A x 1 st V × V A
39 38 eqriv dom A = 1 st V × V A