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

Metamath Proof Explorer

Theorem reusv2lem5

Description: Lemma for reusv2 . (Contributed by NM, 4-Jan-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2lem5 
|- ( ( A. y e. B C e. A /\ B =/= (/) ) -> ( E! x e. A E. y e. B x = C <-> E! x e. A A. y e. B x = C ) )

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 biimt 
 |-  ( ( C e. A /\ T. ) -> ( x = C <-> ( ( C e. A /\ T. ) -> x = C ) ) )
3 1 2 mpan2 
 |-  ( C e. A -> ( x = C <-> ( ( C e. A /\ T. ) -> x = C ) ) )
4 ibar 
 |-  ( C e. A -> ( x = C <-> ( C e. A /\ x = C ) ) )
5 3 4 bitr3d 
 |-  ( C e. A -> ( ( ( C e. A /\ T. ) -> x = C ) <-> ( C e. A /\ x = C ) ) )
6 eleq1 
 |-  ( x = C -> ( x e. A <-> C e. A ) )
7 6 pm5.32ri 
 |-  ( ( x e. A /\ x = C ) <-> ( C e. A /\ x = C ) )
8 5 7 bitr4di 
 |-  ( C e. A -> ( ( ( C e. A /\ T. ) -> x = C ) <-> ( x e. A /\ x = C ) ) )
9 8 ralimi 
 |-  ( A. y e. B C e. A -> A. y e. B ( ( ( C e. A /\ T. ) -> x = C ) <-> ( x e. A /\ x = C ) ) )
10 ralbi 
 |-  ( A. y e. B ( ( ( C e. A /\ T. ) -> x = C ) <-> ( x e. A /\ x = C ) ) -> ( A. y e. B ( ( C e. A /\ T. ) -> x = C ) <-> A. y e. B ( x e. A /\ x = C ) ) )
11 9 10 syl 
 |-  ( A. y e. B C e. A -> ( A. y e. B ( ( C e. A /\ T. ) -> x = C ) <-> A. y e. B ( x e. A /\ x = C ) ) )
12 11 eubidv 
 |-  ( A. y e. B C e. A -> ( E! x A. y e. B ( ( C e. A /\ T. ) -> x = C ) <-> E! x A. y e. B ( x e. A /\ x = C ) ) )
13 r19.28zv 
 |-  ( B =/= (/) -> ( A. y e. B ( x e. A /\ x = C ) <-> ( x e. A /\ A. y e. B x = C ) ) )
14 13 eubidv 
 |-  ( B =/= (/) -> ( E! x A. y e. B ( x e. A /\ x = C ) <-> E! x ( x e. A /\ A. y e. B x = C ) ) )
15 12 14 sylan9bb 
 |-  ( ( A. y e. B C e. A /\ B =/= (/) ) -> ( E! x A. y e. B ( ( C e. A /\ T. ) -> x = C ) <-> E! x ( x e. A /\ A. y e. B x = C ) ) )
16 1 biantrur 
 |-  ( x = C <-> ( T. /\ x = C ) )
17 16 rexbii 
 |-  ( E. y e. B x = C <-> E. y e. B ( T. /\ x = C ) )
18 17 reubii 
 |-  ( E! x e. A E. y e. B x = C <-> E! x e. A E. y e. B ( T. /\ x = C ) )
19 reusv2lem4 
 |-  ( E! x e. A E. y e. B ( T. /\ x = C ) <-> E! x A. y e. B ( ( C e. A /\ T. ) -> x = C ) )
20 18 19 bitri 
 |-  ( E! x e. A E. y e. B x = C <-> E! x A. y e. B ( ( C e. A /\ T. ) -> x = C ) )
21 df-reu 
 |-  ( E! x e. A A. y e. B x = C <-> E! x ( x e. A /\ A. y e. B x = C ) )
22 15 20 21 3bitr4g 
 |-  ( ( A. y e. B C e. A /\ B =/= (/) ) -> ( E! x e. A E. y e. B x = C <-> E! x e. A A. y e. B x = C ) )