Metamath Proof Explorer


Theorem eusvobj2

Description: Specify the same property in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis eusvobj1.1 BV
Assertion eusvobj2 ∃!xyAx=ByAx=ByAx=B

Proof

Step Hyp Ref Expression
1 eusvobj1.1 BV
2 euabsn2 ∃!xyAx=Bzx|yAx=B=z
3 eleq2 x|yAx=B=zxx|yAx=Bxz
4 abid xx|yAx=ByAx=B
5 velsn xzx=z
6 3 4 5 3bitr3g x|yAx=B=zyAx=Bx=z
7 nfre1 yyAx=B
8 7 nfab _yx|yAx=B
9 8 nfeq1 yx|yAx=B=z
10 1 elabrex yABx|yAx=B
11 eleq2 x|yAx=B=zBx|yAx=BBz
12 1 elsn BzB=z
13 eqcom B=zz=B
14 12 13 bitri Bzz=B
15 11 14 bitrdi x|yAx=B=zBx|yAx=Bz=B
16 10 15 syl5ib x|yAx=B=zyAz=B
17 9 16 ralrimi x|yAx=B=zyAz=B
18 eqeq1 x=zx=Bz=B
19 18 ralbidv x=zyAx=ByAz=B
20 17 19 syl5ibrcom x|yAx=B=zx=zyAx=B
21 6 20 sylbid x|yAx=B=zyAx=ByAx=B
22 21 exlimiv zx|yAx=B=zyAx=ByAx=B
23 2 22 sylbi ∃!xyAx=ByAx=ByAx=B
24 euex ∃!xyAx=BxyAx=B
25 rexn0 yAx=BA
26 25 exlimiv xyAx=BA
27 r19.2z AyAx=ByAx=B
28 27 ex AyAx=ByAx=B
29 24 26 28 3syl ∃!xyAx=ByAx=ByAx=B
30 23 29 impbid ∃!xyAx=ByAx=ByAx=B