Metamath Proof Explorer


Theorem 2reuswap2

Description: A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017)

Ref Expression
Assertion 2reuswap2 xA*yyBφ∃!xAyBφ∃!yBxAφ

Proof

Step Hyp Ref Expression
1 df-ral xA*yyBφxxA*yyBφ
2 moanimv *yxAyBφxA*yyBφ
3 2 albii x*yxAyBφxxA*yyBφ
4 1 3 bitr4i xA*yyBφx*yxAyBφ
5 2euswapv x*yxAyBφ∃!xyxAyBφ∃!yxxAyBφ
6 df-reu ∃!xAyBφ∃!xxAyBφ
7 r19.42v yBxAφxAyBφ
8 df-rex yBxAφyyBxAφ
9 7 8 bitr3i xAyBφyyBxAφ
10 an12 yBxAφxAyBφ
11 10 exbii yyBxAφyxAyBφ
12 9 11 bitri xAyBφyxAyBφ
13 12 eubii ∃!xxAyBφ∃!xyxAyBφ
14 6 13 bitri ∃!xAyBφ∃!xyxAyBφ
15 df-reu ∃!yBxAφ∃!yyBxAφ
16 r19.42v xAyBφyBxAφ
17 df-rex xAyBφxxAyBφ
18 16 17 bitr3i yBxAφxxAyBφ
19 18 eubii ∃!yyBxAφ∃!yxxAyBφ
20 15 19 bitri ∃!yBxAφ∃!yxxAyBφ
21 5 14 20 3imtr4g x*yxAyBφ∃!xAyBφ∃!yBxAφ
22 4 21 sylbi xA*yyBφ∃!xAyBφ∃!yBxAφ