Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  refun0 Structured version   Unicode version

Theorem refun0 19889
 Description: Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.)
Assertion
Ref Expression
refun0

Proof of Theorem refun0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2443 . . . 4
2 eqid 2443 . . . 4
31, 2refbas 19884 . . 3
5 elun 3630 . . . 4
6 refssex 19885 . . . . . 6
76adantlr 714 . . . . 5
8 0ss 3800 . . . . . . . . 9
98a1i 11 . . . . . . . 8
109reximdva0 3782 . . . . . . 7
1110adantr 465 . . . . . 6
12 elsni 4039 . . . . . . . 8
13 sseq1 3510 . . . . . . . . 9
1413rexbidv 2954 . . . . . . . 8
1512, 14syl 16 . . . . . . 7
1615adantl 466 . . . . . 6
1711, 16mpbird 232 . . . . 5
187, 17jaodan 785 . . . 4
195, 18sylan2b 475 . . 3
2019ralrimiva 2857 . 2
21 refrel 19882 . . . . . 6
2221brrelexi 5030 . . . . 5
23 p0ex 4624 . . . . 5
24 unexg 6586 . . . . 5
2522, 23, 24sylancl 662 . . . 4
26 uniun 4253 . . . . . 6
27 0ex 4567 . . . . . . . 8
2827unisn 4249 . . . . . . 7
2928uneq2i 3640 . . . . . 6
30 un0 3796 . . . . . 6
3126, 29, 303eqtrri 2477 . . . . 5
3231, 2isref 19883 . . . 4
3325, 32syl 16 . . 3