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

Theorem fiuneneq 27343
 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 958 . . . . . 6
2 enfi 7275 . . . . . . . 8
323ad2ant1 978 . . . . . . 7
41, 3mpbid 202 . . . . . 6
5 unfi 7324 . . . . . 6
61, 4, 5syl2anc 643 . . . . 5
7 ssun1 3467 . . . . . 6
87a1i 11 . . . . 5
9 simp3 959 . . . . . 6
109ensymd 7108 . . . . 5
11 fisseneq 7270 . . . . 5
126, 8, 10, 11syl3anc 1184 . . . 4
13 ssun2 3468 . . . . . 6
1413a1i 11 . . . . 5
15 simp1 957 . . . . . . 7
16 entr 7109 . . . . . . 7
179, 15, 16syl2anc 643 . . . . . 6
1817ensymd 7108 . . . . 5
19 fisseneq 7270 . . . . 5
206, 14, 18, 19syl3anc 1184 . . . 4
2112, 20eqtr4d 2436 . . 3
22213expia 1155 . 2
23 enrefg 7089 . . . 4