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

Theorem iscard2 7810
 Description: Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225. (Contributed by Mario Carneiro, 15-Jan-2013.)
Assertion
Ref Expression
iscard2
Distinct variable group:   ,

Proof of Theorem iscard2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cardon 7778 . . 3
2 eleq1 2461 . . 3
31, 2mpbii 203 . 2
4 cardonle 7791 . . . . . 6
54biantrurd 495 . . . . 5
6 eqss 3320 . . . . 5
75, 6syl6rbbr 256 . . . 4
8 oncardval 7789 . . . . 5
98sseq2d 3333 . . . 4
107, 9bitrd 245 . . 3
11 ssint 4022 . . . 4
12 breq1 4170 . . . . . . . . 9
1312elrab 3049 . . . . . . . 8
14 ensymb 7105 . . . . . . . . 9
1514anbi2i 676 . . . . . . . 8
1613, 15bitri 241 . . . . . . 7
1716imbi1i 316 . . . . . 6
18 impexp 434 . . . . . 6
1917, 18bitri 241 . . . . 5
2019ralbii2 2691 . . . 4
2111, 20bitri 241 . . 3
2210, 21syl6bb 253 . 2