Metamath Proof Explorer

Definition df-2reu

Description: Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023)

Ref Expression
Assertion df-2reu 
|- ( E! x e. A , y e. B ph <-> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 
 |-  x
1 cA 
 |-  A
2 vy 
 |-  y
3 cB 
 |-  B
4 wph 
 |-  ph
5 4 0 2 1 3 w2reu 
 |-  E! x e. A , y e. B ph
6 4 2 3 wrex 
 |-  E. y e. B ph
7 6 0 1 wreu 
 |-  E! x e. A E. y e. B ph
8 4 0 1 wrex 
 |-  E. x e. A ph
9 8 2 3 wreu 
 |-  E! y e. B E. x e. A ph
10 7 9 wa 
 |-  ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph )
11 5 10 wb 
 |-  ( E! x e. A , y e. B ph <-> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) )