Metamath Proof Explorer


Theorem 2reu3

Description: Double restricted existential uniqueness, analogous to 2eu3 . (Contributed by Alexander van der Vekens, 29-Jun-2017)

Ref Expression
Assertion 2reu3 xAyB*xAφ*yBφ∃!xA∃!yBφ∃!yB∃!xAφ∃!xAyBφ∃!yBxAφ

Proof

Step Hyp Ref Expression
1 orcom *xAφ*yBφ*yBφ*xAφ
2 1 ralbii yB*xAφ*yBφyB*yBφ*xAφ
3 nfrmo1 y*yBφ
4 3 r19.32 yB*yBφ*xAφ*yBφyB*xAφ
5 2 4 bitri yB*xAφ*yBφ*yBφyB*xAφ
6 orcom *yBφyB*xAφyB*xAφ*yBφ
7 5 6 bitri yB*xAφ*yBφyB*xAφ*yBφ
8 7 ralbii xAyB*xAφ*yBφxAyB*xAφ*yBφ
9 nfcv _xB
10 nfrmo1 x*xAφ
11 9 10 nfralw xyB*xAφ
12 11 r19.32 xAyB*xAφ*yBφyB*xAφxA*yBφ
13 8 12 bitri xAyB*xAφ*yBφyB*xAφxA*yBφ
14 2reu1 yB*xAφ∃!yB∃!xAφ∃!yBxAφ∃!xAyBφ
15 14 biimpd yB*xAφ∃!yB∃!xAφ∃!yBxAφ∃!xAyBφ
16 ancom ∃!yBxAφ∃!xAyBφ∃!xAyBφ∃!yBxAφ
17 15 16 imbitrdi yB*xAφ∃!yB∃!xAφ∃!xAyBφ∃!yBxAφ
18 17 adantld yB*xAφ∃!xA∃!yBφ∃!yB∃!xAφ∃!xAyBφ∃!yBxAφ
19 2reu1 xA*yBφ∃!xA∃!yBφ∃!xAyBφ∃!yBxAφ
20 19 biimpd xA*yBφ∃!xA∃!yBφ∃!xAyBφ∃!yBxAφ
21 20 adantrd xA*yBφ∃!xA∃!yBφ∃!yB∃!xAφ∃!xAyBφ∃!yBxAφ
22 18 21 jaoi yB*xAφxA*yBφ∃!xA∃!yBφ∃!yB∃!xAφ∃!xAyBφ∃!yBxAφ
23 2rexreu ∃!xAyBφ∃!yBxAφ∃!xA∃!yBφ
24 2rexreu ∃!yBxAφ∃!xAyBφ∃!yB∃!xAφ
25 24 ancoms ∃!xAyBφ∃!yBxAφ∃!yB∃!xAφ
26 23 25 jca ∃!xAyBφ∃!yBxAφ∃!xA∃!yBφ∃!yB∃!xAφ
27 22 26 impbid1 yB*xAφxA*yBφ∃!xA∃!yBφ∃!yB∃!xAφ∃!xAyBφ∃!yBxAφ
28 13 27 sylbi xAyB*xAφ*yBφ∃!xA∃!yBφ∃!yB∃!xAφ∃!xAyBφ∃!yBxAφ