Metamath Proof Explorer

Theorem reusv2lem3

Description: Lemma for reusv2 . (Contributed by NM, 14-Dec-2012) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2lem3 ⊢∀y∈AB∈V→∃!x∃y∈Ax=B↔∃!x∀y∈Ax=B

Proof

Step Hyp Ref Expression
1 simpr ⊢∀y∈AB∈V∧∃!x∃y∈Ax=B→∃!x∃y∈Ax=B
2 nfv ⊢Ⅎx∀y∈AB∈V
3 nfeu1 ⊢Ⅎx∃!x∃y∈Ax=B
4 2 3 nfan ⊢Ⅎx∀y∈AB∈V∧∃!x∃y∈Ax=B
5 euex ⊢∃!x∃y∈Ax=B→∃x∃y∈Ax=B
6 rexn0 ⊢∃y∈Ax=B→A≠∅
7 6 exlimiv ⊢∃x∃y∈Ax=B→A≠∅
8 r19.2z ⊢A≠∅∧∀y∈Ax=B→∃y∈Ax=B
9 8 ex ⊢A≠∅→∀y∈Ax=B→∃y∈Ax=B
10 5 7 9 3syl ⊢∃!x∃y∈Ax=B→∀y∈Ax=B→∃y∈Ax=B
11 10 adantl ⊢∀y∈AB∈V∧∃!x∃y∈Ax=B→∀y∈Ax=B→∃y∈Ax=B
12 nfra1 ⊢Ⅎy∀y∈AB∈V
13 nfre1 ⊢Ⅎy∃y∈Ax=B
14 13 nfeuw ⊢Ⅎy∃!x∃y∈Ax=B
15 12 14 nfan ⊢Ⅎy∀y∈AB∈V∧∃!x∃y∈Ax=B
16 rsp ⊢∀y∈AB∈V→y∈A→B∈V
17 16 impcom ⊢y∈A∧∀y∈AB∈V→B∈V
18 isset ⊢B∈V↔∃xx=B
19 17 18 sylib ⊢y∈A∧∀y∈AB∈V→∃xx=B
20 19 adantrr ⊢y∈A∧∀y∈AB∈V∧∃!x∃y∈Ax=B→∃xx=B
21 rspe ⊢y∈A∧x=B→∃y∈Ax=B
22 21 ex ⊢y∈A→x=B→∃y∈Ax=B
23 22 ancrd ⊢y∈A→x=B→∃y∈Ax=B∧x=B
24 23 eximdv ⊢y∈A→∃xx=B→∃x∃y∈Ax=B∧x=B
25 24 imp ⊢y∈A∧∃xx=B→∃x∃y∈Ax=B∧x=B
26 20 25 syldan ⊢y∈A∧∀y∈AB∈V∧∃!x∃y∈Ax=B→∃x∃y∈Ax=B∧x=B
27 eupick ⊢∃!x∃y∈Ax=B∧∃x∃y∈Ax=B∧x=B→∃y∈Ax=B→x=B
28 1 26 27 syl2an2 ⊢y∈A∧∀y∈AB∈V∧∃!x∃y∈Ax=B→∃y∈Ax=B→x=B
29 28 ex ⊢y∈A→∀y∈AB∈V∧∃!x∃y∈Ax=B→∃y∈Ax=B→x=B
30 29 com3l ⊢∀y∈AB∈V∧∃!x∃y∈Ax=B→∃y∈Ax=B→y∈A→x=B
31 15 13 30 ralrimd ⊢∀y∈AB∈V∧∃!x∃y∈Ax=B→∃y∈Ax=B→∀y∈Ax=B
32 11 31 impbid ⊢∀y∈AB∈V∧∃!x∃y∈Ax=B→∀y∈Ax=B↔∃y∈Ax=B
33 4 32 eubid ⊢∀y∈AB∈V∧∃!x∃y∈Ax=B→∃!x∀y∈Ax=B↔∃!x∃y∈Ax=B
34 1 33 mpbird ⊢∀y∈AB∈V∧∃!x∃y∈Ax=B→∃!x∀y∈Ax=B
35 34 ex ⊢∀y∈AB∈V→∃!x∃y∈Ax=B→∃!x∀y∈Ax=B
36 reusv2lem2 ⊢∃!x∀y∈Ax=B→∃!x∃y∈Ax=B
37 35 36 impbid1 ⊢∀y∈AB∈V→∃!x∃y∈Ax=B↔∃!x∀y∈Ax=B