Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ener Unicode version

Theorem ener 6639
 Description: Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
ener

Proof of Theorem ener
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relen 6604 . . . 4
21a1i 9 . . 3
3 bren 6607 . . . . 5
4 f1ocnv 5346 . . . . . . 7
5 vex 2661 . . . . . . . 8
6 vex 2661 . . . . . . . 8
7 f1oen2g 6615 . . . . . . . 8
85, 6, 7mp3an12 1288 . . . . . . 7
94, 8syl 14 . . . . . 6
109exlimiv 1560 . . . . 5
113, 10sylbi 120 . . . 4
13 bren 6607 . . . . 5
14 bren 6607 . . . . 5
15 eeanv 1882 . . . . . 6
16 f1oco 5356 . . . . . . . . 9
1716ancoms 266 . . . . . . . 8
18 vex 2661 . . . . . . . . 9
19 f1oen2g 6615 . . . . . . . . 9
206, 18, 19mp3an12 1288 . . . . . . . 8
2117, 20syl 14 . . . . . . 7
2221exlimivv 1850 . . . . . 6
2315, 22sylbir 134 . . . . 5
2413, 14, 23syl2anb 287 . . . 4