Metamath Proof Explorer


Theorem unirep

Description: Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011)

Ref Expression
Hypotheses unirep.1 y=Dφψ
unirep.2 y=DB=C
unirep.3 y=zφχ
unirep.4 y=zB=F
unirep.5 BV
Assertion unirep yAzAφχB=FDAψιx|yAφx=B=C

Proof

Step Hyp Ref Expression
1 unirep.1 y=Dφψ
2 unirep.2 y=DB=C
3 unirep.3 y=zφχ
4 unirep.4 y=zB=F
5 unirep.5 BV
6 eqidd ψC=C
7 6 ancli ψψC=C
8 2 eqeq2d y=DC=BC=C
9 1 8 anbi12d y=DφC=BψC=C
10 9 rspcev DAψC=CyAφC=B
11 7 10 sylan2 DAψyAφC=B
12 11 adantl yAzAφχB=FDAψyAφC=B
13 nfcvd DA_yC
14 13 2 csbiegf DAD/yB=C
15 5 csbex D/yBV
16 14 15 eqeltrrdi DACV
17 16 ad2antrl yAzAφχB=FDAψCV
18 eqeq1 x=Cx=BC=B
19 18 anbi2d x=Cφx=BφC=B
20 19 rexbidv x=CyAφx=ByAφC=B
21 20 spcegv CVyAφC=BxyAφx=B
22 16 21 syl DAyAφC=BxyAφx=B
23 22 adantr DAψyAφC=BxyAφx=B
24 11 23 mpd DAψxyAφx=B
25 24 adantl yAzAφχB=FDAψxyAφx=B
26 r19.29 yAzAφχB=FyAφx=ByAzAφχB=Fφx=B
27 r19.29 zAφχB=FzAχw=FzAφχB=Fχw=F
28 an4 φx=Bχw=Fφχx=Bw=F
29 pm3.35 φχφχB=FB=F
30 eqeq12 x=Bw=Fx=wB=F
31 29 30 syl5ibrcom φχφχB=Fx=Bw=Fx=w
32 31 ancoms φχB=Fφχx=Bw=Fx=w
33 32 expimpd φχB=Fφχx=Bw=Fx=w
34 28 33 syl5bi φχB=Fφx=Bχw=Fx=w
35 34 ancomsd φχB=Fχw=Fφx=Bx=w
36 35 expdimp φχB=Fχw=Fφx=Bx=w
37 36 rexlimivw zAφχB=Fχw=Fφx=Bx=w
38 37 imp zAφχB=Fχw=Fφx=Bx=w
39 27 38 sylan zAφχB=FzAχw=Fφx=Bx=w
40 39 an32s zAφχB=Fφx=BzAχw=Fx=w
41 40 ex zAφχB=Fφx=BzAχw=Fx=w
42 41 rexlimivw yAzAφχB=Fφx=BzAχw=Fx=w
43 26 42 syl yAzAφχB=FyAφx=BzAχw=Fx=w
44 43 expimpd yAzAφχB=FyAφx=BzAχw=Fx=w
45 44 adantr yAzAφχB=FDAψyAφx=BzAχw=Fx=w
46 45 alrimivv yAzAφχB=FDAψxwyAφx=BzAχw=Fx=w
47 eqeq1 x=wx=Bw=B
48 47 anbi2d x=wφx=Bφw=B
49 48 rexbidv x=wyAφx=ByAφw=B
50 4 eqeq2d y=zw=Bw=F
51 3 50 anbi12d y=zφw=Bχw=F
52 51 cbvrexvw yAφw=BzAχw=F
53 49 52 bitrdi x=wyAφx=BzAχw=F
54 53 eu4 ∃!xyAφx=BxyAφx=BxwyAφx=BzAχw=Fx=w
55 25 46 54 sylanbrc yAzAφχB=FDAψ∃!xyAφx=B
56 20 iota2 CV∃!xyAφx=ByAφC=Bιx|yAφx=B=C
57 17 55 56 syl2anc yAzAφχB=FDAψyAφC=Bιx|yAφx=B=C
58 12 57 mpbid yAzAφχB=FDAψιx|yAφx=B=C