Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fiuneneq Unicode version

Theorem fiuneneq 27513
 Description: Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.)
Assertion
Ref Expression
fiuneneq

Proof of Theorem fiuneneq
StepHypRef Expression
1 simp2 956 . . . . . 6
2 enfi 7079 . . . . . . . 8
323ad2ant1 976 . . . . . . 7
41, 3mpbid 201 . . . . . 6
5 unfi 7124 . . . . . 6
61, 4, 5syl2anc 642 . . . . 5
7 ssun1 3338 . . . . . 6
87a1i 10 . . . . 5
9 simp3 957 . . . . . 6
10 ensym 6910 . . . . . 6
119, 10syl 15 . . . . 5
12 fisseneq 7074 . . . . 5
136, 8, 11, 12syl3anc 1182 . . . 4
14 ssun2 3339 . . . . . 6
1514a1i 10 . . . . 5
16 simp1 955 . . . . . . 7
17 entr 6913 . . . . . . 7
189, 16, 17syl2anc 642 . . . . . 6
19 ensym 6910 . . . . . 6
2018, 19syl 15 . . . . 5
21 fisseneq 7074 . . . . 5
226, 15, 20, 21syl3anc 1182 . . . 4
2313, 22eqtr4d 2318 . . 3
24233expia 1153 . 2
25 enrefg 6893 . . . 4