Metamath Proof Explorer


Theorem reusv2lem5

Description: Lemma for reusv2 . (Contributed by NM, 4-Jan-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2lem5 y B C A B ∃! x A y B x = C ∃! x A y B x = C

Proof

Step Hyp Ref Expression
1 tru
2 biimt C A x = C C A x = C
3 1 2 mpan2 C A x = C C A x = C
4 ibar C A x = C C A x = C
5 3 4 bitr3d C A C A x = C C A x = C
6 eleq1 x = C x A C A
7 6 pm5.32ri x A x = C C A x = C
8 5 7 bitr4di C A C A x = C x A x = C
9 8 ralimi y B C A y B C A x = C x A x = C
10 ralbi y B C A x = C x A x = C y B C A x = C y B x A x = C
11 9 10 syl y B C A y B C A x = C y B x A x = C
12 11 eubidv y B C A ∃! x y B C A x = C ∃! x y B x A x = C
13 r19.28zv B y B x A x = C x A y B x = C
14 13 eubidv B ∃! x y B x A x = C ∃! x x A y B x = C
15 12 14 sylan9bb y B C A B ∃! x y B C A x = C ∃! x x A y B x = C
16 1 biantrur x = C x = C
17 16 rexbii y B x = C y B x = C
18 17 reubii ∃! x A y B x = C ∃! x A y B x = C
19 reusv2lem4 ∃! x A y B x = C ∃! x y B C A x = C
20 18 19 bitri ∃! x A y B x = C ∃! x y B C A x = C
21 df-reu ∃! x A y B x = C ∃! x x A y B x = C
22 15 20 21 3bitr4g y B C A B ∃! x A y B x = C ∃! x A y B x = C