Theorem reusv2lem2

Description: Lemma for reusv2 . (Contributed by NM, 27-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

	Ref	Expression
Assertion	reusv2lem2	|- ( E! x A. y e. A x = B -> E! x E. y e. A x = B )

Proof

Step	Hyp	Ref	Expression
1		eunex	|- ( E! x A. y e. A x = B -> E. x -. A. y e. A x = B )
2		exnal	|- ( E. x -. A. y e. A x = B <-> -. A. x A. y e. A x = B )
3	1 2	sylib	|- ( E! x A. y e. A x = B -> -. A. x A. y e. A x = B )
4		rzal	|- ( A = (/) -> A. y e. A x = B )
5	4	alrimiv	|- ( A = (/) -> A. x A. y e. A x = B )
6	3 5	nsyl3	|- ( A = (/) -> -. E! x A. y e. A x = B )
7	6	pm2.21d	|- ( A = (/) -> ( E! x A. y e. A x = B -> E! x E. y e. A x = B ) )
8		simpr	|- ( ( A =/= (/) /\ E! x A. y e. A x = B ) -> E! x A. y e. A x = B )
9		nfra1	|- F/ y A. y e. A z = B
10		nfra1	|- F/ y A. y e. A x = B
11		simpr	|- ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> x = B )
12		rspa	|- ( ( A. y e. A z = B /\ y e. A ) -> z = B )
13	12	adantr	|- ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> z = B )
14	11 13	eqtr4d	|- ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> x = z )
15		eqeq1	|- ( x = z -> ( x = B <-> z = B ) )
16	15	ralbidv	|- ( x = z -> ( A. y e. A x = B <-> A. y e. A z = B ) )
17	16	biimprcd	|- ( A. y e. A z = B -> ( x = z -> A. y e. A x = B ) )
18	17	ad2antrr	|- ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> ( x = z -> A. y e. A x = B ) )
19	14 18	mpd	|- ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> A. y e. A x = B )
20	19	exp31	|- ( A. y e. A z = B -> ( y e. A -> ( x = B -> A. y e. A x = B ) ) )
21	9 10 20	rexlimd	|- ( A. y e. A z = B -> ( E. y e. A x = B -> A. y e. A x = B ) )
22	21	adantl	|- ( ( A =/= (/) /\ A. y e. A z = B ) -> ( E. y e. A x = B -> A. y e. A x = B ) )
23		r19.2z	|- ( ( A =/= (/) /\ A. y e. A x = B ) -> E. y e. A x = B )
24	23	ex	|- ( A =/= (/) -> ( A. y e. A x = B -> E. y e. A x = B ) )
25	24	adantr	|- ( ( A =/= (/) /\ A. y e. A z = B ) -> ( A. y e. A x = B -> E. y e. A x = B ) )
26	22 25	impbid	|- ( ( A =/= (/) /\ A. y e. A z = B ) -> ( E. y e. A x = B <-> A. y e. A x = B ) )
27	26	eubidv	|- ( ( A =/= (/) /\ A. y e. A z = B ) -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) )
28	27	ex	|- ( A =/= (/) -> ( A. y e. A z = B -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) ) )
29	28	exlimdv	|- ( A =/= (/) -> ( E. z A. y e. A z = B -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) ) )
30		euex	|- ( E! x A. y e. A x = B -> E. x A. y e. A x = B )
31	16	cbvexvw	|- ( E. x A. y e. A x = B <-> E. z A. y e. A z = B )
32	30 31	sylib	|- ( E! x A. y e. A x = B -> E. z A. y e. A z = B )
33	29 32	impel	|- ( ( A =/= (/) /\ E! x A. y e. A x = B ) -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) )
34	8 33	mpbird	|- ( ( A =/= (/) /\ E! x A. y e. A x = B ) -> E! x E. y e. A x = B )
35	34	ex	|- ( A =/= (/) -> ( E! x A. y e. A x = B -> E! x E. y e. A x = B ) )
36	7 35	pm2.61ine	|- ( E! x A. y e. A x = B -> E! x E. y e. A x = B )