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

Metamath Proof Explorer

Theorem 2reu4

Description: Definition of double restricted existential uniqueness ("exactly one x and exactly one y "), analogous to 2eu4 . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion 2reu4 
|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) )

Proof

Step Hyp Ref Expression
1 reurex 
 |-  ( E! x e. A E. y e. B ph -> E. x e. A E. y e. B ph )
2 rexn0 
 |-  ( E. x e. A E. y e. B ph -> A =/= (/) )
3 1 2 syl 
 |-  ( E! x e. A E. y e. B ph -> A =/= (/) )
4 reurex 
 |-  ( E! y e. B E. x e. A ph -> E. y e. B E. x e. A ph )
5 rexn0 
 |-  ( E. y e. B E. x e. A ph -> B =/= (/) )
6 4 5 syl 
 |-  ( E! y e. B E. x e. A ph -> B =/= (/) )
7 3 6 anim12i 
 |-  ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) -> ( A =/= (/) /\ B =/= (/) ) )
8 ne0i 
 |-  ( x e. A -> A =/= (/) )
9 ne0i 
 |-  ( y e. B -> B =/= (/) )
10 8 9 anim12i 
 |-  ( ( x e. A /\ y e. B ) -> ( A =/= (/) /\ B =/= (/) ) )
11 10 a1d 
 |-  ( ( x e. A /\ y e. B ) -> ( ph -> ( A =/= (/) /\ B =/= (/) ) ) )
12 11 rexlimivv 
 |-  ( E. x e. A E. y e. B ph -> ( A =/= (/) /\ B =/= (/) ) )
13 12 adantr 
 |-  ( ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) -> ( A =/= (/) /\ B =/= (/) ) )
14 2reu4lem 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) )
15 7 13 14 pm5.21nii 
 |-  ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) )