Description: Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | enfi | |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enen1 | |- ( A ~~ B -> ( A ~~ x <-> B ~~ x ) ) |
|
2 | 1 | rexbidv | |- ( A ~~ B -> ( E. x e. _om A ~~ x <-> E. x e. _om B ~~ x ) ) |
3 | isfi | |- ( A e. Fin <-> E. x e. _om A ~~ x ) |
|
4 | isfi | |- ( B e. Fin <-> E. x e. _om B ~~ x ) |
|
5 | 2 3 4 | 3bitr4g | |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) ) |