# Metamath Proof Explorer

## Theorem cardval3

Description: An alternate definition of the value of ( cardA ) that does not require AC to prove. (Contributed by Mario Carneiro, 7-Jan-2013) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion cardval3
`|- ( A e. dom card -> ( card ` A ) = |^| { x e. On | x ~~ A } )`

### Proof

Step Hyp Ref Expression
1 elex
` |-  ( A e. dom card -> A e. _V )`
2 isnum2
` |-  ( A e. dom card <-> E. x e. On x ~~ A )`
3 rabn0
` |-  ( { x e. On | x ~~ A } =/= (/) <-> E. x e. On x ~~ A )`
4 intex
` |-  ( { x e. On | x ~~ A } =/= (/) <-> |^| { x e. On | x ~~ A } e. _V )`
5 2 3 4 3bitr2i
` |-  ( A e. dom card <-> |^| { x e. On | x ~~ A } e. _V )`
6 5 biimpi
` |-  ( A e. dom card -> |^| { x e. On | x ~~ A } e. _V )`
7 breq2
` |-  ( y = A -> ( x ~~ y <-> x ~~ A ) )`
8 7 rabbidv
` |-  ( y = A -> { x e. On | x ~~ y } = { x e. On | x ~~ A } )`
9 8 inteqd
` |-  ( y = A -> |^| { x e. On | x ~~ y } = |^| { x e. On | x ~~ A } )`
10 df-card
` |-  card = ( y e. _V |-> |^| { x e. On | x ~~ y } )`
11 9 10 fvmptg
` |-  ( ( A e. _V /\ |^| { x e. On | x ~~ A } e. _V ) -> ( card ` A ) = |^| { x e. On | x ~~ A } )`
12 1 6 11 syl2anc
` |-  ( A e. dom card -> ( card ` A ) = |^| { x e. On | x ~~ A } )`