Metamath Proof Explorer


Theorem 2reu5lem3

Description: Lemma for 2reu5 . This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Assertion 2reu5lem3 ∃!xA∃!yBφxA*yBφxAyBφzwxAyBφx=zy=w

Proof

Step Hyp Ref Expression
1 2reu5lem1 ∃!xA∃!yBφ∃!x∃!yxAyBφ
2 2reu5lem2 xA*yBφx*yxAyBφ
3 1 2 anbi12i ∃!xA∃!yBφxA*yBφ∃!x∃!yxAyBφx*yxAyBφ
4 2eu5 ∃!x∃!yxAyBφx*yxAyBφxyxAyBφzwxyxAyBφx=zy=w
5 3anass xAyBφxAyBφ
6 5 exbii yxAyBφyxAyBφ
7 19.42v yxAyBφxAyyBφ
8 df-rex yBφyyBφ
9 8 bicomi yyBφyBφ
10 9 anbi2i xAyyBφxAyBφ
11 6 7 10 3bitri yxAyBφxAyBφ
12 11 exbii xyxAyBφxxAyBφ
13 df-rex xAyBφxxAyBφ
14 12 13 bitr4i xyxAyBφxAyBφ
15 3anan12 xAyBφyBxAφ
16 15 imbi1i xAyBφx=zy=wyBxAφx=zy=w
17 impexp yBxAφx=zy=wyBxAφx=zy=w
18 impexp xAφx=zy=wxAφx=zy=w
19 18 imbi2i yBxAφx=zy=wyBxAφx=zy=w
20 16 17 19 3bitri xAyBφx=zy=wyBxAφx=zy=w
21 20 albii yxAyBφx=zy=wyyBxAφx=zy=w
22 df-ral yBxAφx=zy=wyyBxAφx=zy=w
23 r19.21v yBxAφx=zy=wxAyBφx=zy=w
24 21 22 23 3bitr2i yxAyBφx=zy=wxAyBφx=zy=w
25 24 albii xyxAyBφx=zy=wxxAyBφx=zy=w
26 df-ral xAyBφx=zy=wxxAyBφx=zy=w
27 25 26 bitr4i xyxAyBφx=zy=wxAyBφx=zy=w
28 27 exbii wxyxAyBφx=zy=wwxAyBφx=zy=w
29 28 exbii zwxyxAyBφx=zy=wzwxAyBφx=zy=w
30 14 29 anbi12i xyxAyBφzwxyxAyBφx=zy=wxAyBφzwxAyBφx=zy=w
31 3 4 30 3bitri ∃!xA∃!yBφxA*yBφxAyBφzwxAyBφx=zy=w