This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2reu5a

Description: Double restricted existential uniqueness in terms of restricted existence and restricted "at most one". (Contributed by Alexander van der Vekens, 17-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 reu5 
 |-  ( E! x e. A E! y e. B ph <-> ( E. x e. A E! y e. B ph /\ E* x e. A E! y e. B ph ) )
2 reu5 
 |-  ( E! y e. B ph <-> ( E. y e. B ph /\ E* y e. B ph ) )
3 2 rexbii 
 |-  ( E. x e. A E! y e. B ph <-> E. x e. A ( E. y e. B ph /\ E* y e. B ph ) )
4 2 rmobii 
 |-  ( E* x e. A E! y e. B ph <-> E* x e. A ( E. y e. B ph /\ E* y e. B ph ) )
5 3 4 anbi12i 
 |-  ( ( E. x e. A E! y e. B ph /\ E* x e. A E! y e. B ph ) <-> ( E. x e. A ( E. y e. B ph /\ E* y e. B ph ) /\ E* x e. A ( E. y e. B ph /\ E* y e. B ph ) ) )
6 1 5 bitri 
 |-  ( E! x e. A E! y e. B ph <-> ( E. x e. A ( E. y e. B ph /\ E* y e. B ph ) /\ E* x e. A ( E. y e. B ph /\ E* y e. B ph ) ) )